Modeling Advice: Capturing Safety Properties

[Daniel Way]

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))

====

[Stephan Merz]

Welcome to the TLA+ community!

I indeed believe that the properties that you are interested in are best verified in a refinement style where the high-level specification "obviously" enforces the conditions (along the lines of the spec that you included in your message), and then verify that a lower-level description of the actual system implies the higher-level spec. The write-through cache example in chapter 5 of Specifying Systems follows this strategy.

A few remarks about the spec that you sent:

- SectorBytes could be an operator or a function. It doesn’t make a huge difference, but when in doubt, I’d rather use an operator.

- The definition of ByteRange is short and the operator is only used at a single place of the spec, you may consider inlining it.

- The second property asserts that "A flash location may not be written more than once without an  interposed erase". This condition is ensured by two guards in the Write action: first you require that all relevant sectors have a state different from "unknown", then that Programmed \cap Bytes = {}. I believe indeed that this ensures what you want because I think that you have the invariant

\A s \in Sectors : SectorBytes[s] \cap Programmed # {} => SectorState[s] = "programmed"

which (together with the type invariant) implies that the relevant sectors must have been erased, but why not make it more explicit by replacing the two guards by

\A s \in WriteSectors : SectorState[s] = "erased"

in the definition of Write? (And in fact this change would make it obvious that both properties of interest are ensured by the high-level specification.) Perhaps one could even get rid of the variable Programmed and let the high-level spec exclusively focus on sectors, given that this is the only concept that appears in the properties that you describe.

My 2 cents,

Stephan

--
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+u...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/e14dd319-6f38-421a-9259-fe0bd08d119dn%40googlegroups.com.

[Daniel Way]

Thank you, Stephan, for your helpful input and advice.

I'm updating my specification to make SectorBytes an operator and inline the definition of ByteRange as you suggested. Is the preference towards operators an optimization for time or memory usage?

Regarding the replacement of the two guards with  \A s \in WriteSectors : SectorState[s] = "erased",  I can write to any unwritten address even if the sector has previously been written two. I thought a tristate would indicate this, but you're right that it could be clearer.

Looking again, "erased" is redundant since that state can be deduced from the Programmed set. I only need to track two states then, "unknown" indicating my address does not know the state of a sector, and "programmable" if the programmed locations in the sector are known. This allows the addition of a CheckProgrammable(s) operator which can set the state to "programmable" if none of the bytes in a sector are written. Then changing the initialization to Programmed \in SUBSET AddressSpace means I can check if a region is programmable without having to erase it (a hardware optimization I'd like to include).

I really appreciate your suggestions. I'll reread the write-through cache example to get a better idea how to write a refinement of my first spec.

Best regards,

Daniel

[Stephan Merz]

For a discussion about functions vs. operators, see section 6.4 of Specifying Systems. As I should have made clearer in my original reply, my preference for operators (when you have the choice) is purely personal and not grounded in efficiency concerns.

Stephan

To view this discussion visit https://groups.google.com/d/msgid/tlaplus/6bdfc51e-b221-4da1-b29d-29c9a1a75d07n%40googlegroups.com.