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,StephanOn 28 Jan 2026, at 18:49, Daniel Way <p.wa...@xxxxxxxxx> wrote: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.
- Receive a sequence of data to write to the memory address space
- Erase a sector (contiguous address range) before writing
- 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: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.
- A flash sector must be erased before its locations can be written
- A flash location may not be written more than once without an interposed erase
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, IntegersCONSTANTS N, LengthVARIABLES Programmed, SectorStateASSUME N \in Nat /\ Length \in Nat----Sectors == 1..NAddressSpace == 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+u...@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/e14dd319-6f38-421a-9259-fe0bd08d119dn%40googlegroups.com.