[tlaplus] Modeling Advice: Capturing Safety Properties

[Daniel Way <p.waydan@xxxxxxxxx>]

I'm an embedded software developer and recently started learning TLA+. Common practice at my company is to write block diagrams as informal specifications. I see potential in adding tool-assisted formal specifications written in TLA+ or, perhaps, another language.

I've read through chapter 8 of the Specifying Systems book and the learntla.com tutorial, but - to get more hands-on experience - I'm trying to create a simple specification for a flash memory programming interface. The subsystem will marshal incoming data and perform the following actions.

1. Receive a sequence of data to write to the memory address space
2. Erase a sector (contiguous address range) before writing
3. Validate write requests and report error conditions (out of bounds, or double write).

There are two main safety properties I'd like this system to check: 

1. A flash sector must be erased before its locations can be written
2. A flash location may not be written more than once without an  interposed erase

I think these cases can only be detected during a transition which begs the question, how should I model it? I see Action Properties are one option, but what I've tried first is to write a lower-level specification to model an abstract flash chip (see below). In this model, I guard against writing an already written location and any sector must be erased before I can write to it. My purpose is to instantiate this FlashMemory module in my programming subsystem and call the Write and Erase operators.

I could use advice from more experienced users regarding the following:

• Is making safety property violations illegal (and checking for deadlock) a good way to write a specification?
• Is it better to explicitly check for invalid transitions?
• I'm checking my FlashMemory module by making sure it never deadlocks using the Next definition (similar to the FIFO example in Specifying Systems). Is this a useful way to check the implementation of a submodule or do you recommend other approaches?

Thank you for any suggestions or advice.

Daniel Way

---- MODULE FlashMemory ----

EXTENDS TLC, Naturals, Integers

CONSTANTS N, Length

VARIABLES Programmed, SectorState

ASSUME N \in Nat /\ Length \in Nat

----

Sectors == 1..N

AddressSpace == 1..(N * Length)

----

Init == /\ Programmed = {}

/\ SectorState = [i \in Sectors |-> "unknown"]

TypeOk == /\ Programmed \subseteq AddressSpace

/\ \A s \in Sectors :SectorState[s] \in {"unknown", "erased", "programmed"}

SectorBytes == [s \in Sectors |-> (1 + (s-1)*Length)..(s*Length)]

ByteRange(start, n) == start..(start+n-1)

Write(start, n) == LET Bytes == ByteRange(start, n)

WriteSectors == {s \in Sectors : SectorBytes[s] \cap Bytes /= {}}

IN

/\ Bytes \subseteq AddressSpace \* Cannot write outside the range

/\ \A s \in WriteSectors : SectorState[s] /= "unknown" \* Only program sectors in a known state

/\ Programmed \cap Bytes = {} \* Cannot reprogram locations

/\ SectorState' = [s \in WriteSectors |-> "programmed"] @@ SectorState

/\ Programmed' = Programmed \cup Bytes

(* Erase a sector, clearing all programmed locations and setting the sector state *)

Erase(s) == /\ SectorState' = [SectorState EXCEPT ![s] = "erased"]

/\ Programmed' = Programmed \ SectorBytes[s]

Next == (\E start, len \in AddressSpace : Write(start, len)) \/ (\E sect \in Sectors : Erase(sect))

====

-- 
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/e14dd319-6f38-421a-9259-fe0bd08d119dn%40googlegroups.com.