From informal spec to checkable property

This is the reader companion to the deck. The deck is the primary material: each idea below is one live widget with controls, a picture, the formula with your current values, a one-line readout and an "In words" line. This note gives the derivations and the numbers behind each widget default, in deck order. Every number comes from workbook.ipynb (numpy, scipy and matplotlib only), and a widget at its default state shows the same number: same formula, same defaults, same seed. Every scenario is a toy with stated assumptions. Nothing here is a measurement.

Conventions. A transition system is \mathcal T=(S,S_0,\rightarrow). A trace is \sigma=s_0s_1s_2\ldots with s_0\in S_0 and s_t\rightarrow s_{t+1}. A property P is a set of traces. Random draws come from one 32-bit linear congruential generator, s\leftarrow(1664525\,s+1013904223)\bmod 2^{32}, u=(s+0.5)/2^{32}, with seed 7 everywhere. The occupancy model draws one u for the arrival each step (even when a guard rejects it), then one u per current occupant, in index order.

1. Two questions: did we build it right, did we build the right thing

Idea. Verification checks a model against a property. Validation checks the model against the world. A model checker is "an algorithmic technique to verify a system description against a specification" (wedyan2017_50ae ↗, section III). It cannot see a part of reality that the model does not contain. Modelling is where we "eliminate misunderstandings, inconsistencies, and specification gaps" (abrial2010_b911 ↗, Introduction).

The scenario is a room with an admission guard at its main door. The informal spec is: the room never holds more than C people. The model has the guard. The world has the same guard plus a side door that nobody guards:

with A_t\sim\mathrm{Bern}(p_a), D_t\sim\mathrm{Bin}(\mathrm{occ}_t,p_\ell) and B_t\sim\mathrm{Bern}(q). The model satisfies \mathrm{Traces}(\mathcal T_{\text{model}})\subseteq P by a proof (section 3). The world does not: from occupancy C the guard rejects the main-door arrival, but a side-door arrival with no departure gives C+1.

In words: the proof is true of the model, and the world has a door the model never mentions.

Worked numbers (widget default). C=12, p_a=0.9, p_\ell=0.07, q=0.10, 300 steps, seed 7. The model's largest occupancy is 12, and it sits at capacity for 62 of the 300 steps. The world first crosses the line at step 31 with occupancy 13, and spends 16 of the 300 steps over capacity. At q=0 the world's trace equals the model's trace exactly.

Break it. Switch the side door on (the default) and the proof stays green while the world goes red. Switch it off and the two traces coincide; the proof then covers the world, but only because we made the world match. That is validation, done by hand.

Concept check. A colleague says: "our model passed 4,000 checked properties, therefore the room is safe". Name the two gaps. (The properties were proved of the model, not the room. And the 4,000 you thought of say nothing about the one you did not think of.)

2. The cheapest formal spec: a schema

Idea. A typed schema defines which inputs exist at all. A wrong input is not detected at run time: it is never representable. Rodin's static checker does the same for Event-B models. One of its two objectives is "to filter elements of a model that are not well-formed", and the proof obligation generator works only on what it lets through (abrial2010_b911 ↗, section "On the role of the static checker").

The toy is a scheduling file for a building-visitor simulator. The English says: after dwelling in a room, the visitor walks to its next target. A faithful transcription writes the field after_dwell; the schema calls it after. Both are faithful readings of the same sentence, so a prose review would not catch it. A second slip: a target of kind exit is legal as a state intent and illegal as a walking-leg target.

Write F=\{\text{after},\text{after\_dwell},\text{delay}\} for the field names, K=\{\text{room},\text{door},\text{waypoint},\text{exit}\} for the target kinds and S=\{\text{leg},\text{intent}\} for the slots. The representable configurations are

In words: the schema shrinks the set of models before any state or transition exists.

Worked numbers. |F\times K\times S|=3\times4\times2=24 and |V|=1\times(3+4)=7, so 7/24=0.292 of the configurations are representable. Of three example legs (one correct, one with after_dwell, one with kind exit), 2 of 3 are rejected. With the schema off, the unknown field is dropped without a message and the leg runs with the toy's default wait of 0 s instead of the 30 s the spec said. The 0 s default is a stated toy assumption.

Break it. Switch the schema check off and watch nothing fail loudly. The silence is the bug.

Concept check. The schema rejected exit in one slot and accepted it in another. What did it change: the states, the transitions, or something before either? (Something before either: which configurations exist as inputs. The same value in two slots is two different points of the space.)

3. Safety: one bad state, a finite witness

Idea. A property P is a safety property when every violating trace has a finite bad prefix: if \sigma\notin P there is a k such that no extension of \sigma[0..k] lies in P. One bad step ends the argument, and nothing later can repair it. A counterexample is a single trace \sigma\in\mathrm{Traces}(\mathcal T)\setminus P.

The model, symbol by symbol. S=\{0,1,2,\ldots\}, S_0=\{0\}. Each step A_t\sim\mathrm{Bern}(p_a) and D_t\sim\mathrm{Bin}(\mathrm{occ}_t,p_\ell), and \mathrm{occ}_{t+1}=\mathrm{occ}_t+A_t-D_t. The requirement is \varphi_{\text{safe}}:\ \forall t\ \mathrm{occ}_t\le C.

Read the drift before simulating. Given \mathrm{occ}_t=n,

In words: the room fills while fewer than n^* people are inside and drains above that. Here n^*=12.857>12, so the equilibrium sits above the capacity line and the invariant is doomed before any simulation. At capacity the drift is d(12)=0.9-12\times0.07=+0.06: the room still fills.

The guard and the proof. Replace the transition by \mathrm{occ}_{t+1}=\mathrm{occ}_t+A_t\,\mathbf 1[\mathrm{occ}_t<C]-D_t. Induction on t: \mathrm{occ}_0=0\le C. If \mathrm{occ}_t\le C and \mathrm{occ}_t<C then \mathrm{occ}_{t+1}\le\mathrm{occ}_t+1\le C; if \mathrm{occ}_t=C the guard blocks the arrival, so \mathrm{occ}_{t+1}\le C. The reachable set is \{0,\ldots,C\} by construction.

In words: the guard removes the arrow into C+1, so no trace can contain it. That is a proof, and it needs no samples. It is the schema idea lifted from configurations to behaviours. A bounded Petri net has the same shape: a net "is bounded and thus R(M0) is finite" exactly when no ω appears in its coverability tree, and safeness is glossed as "absence of overflows" (murata1989_d3ec ↗, sections V-A and VII-B), a preview of week 6.

Worked numbers (widget default). Unguarded, seed 7, C=12: the first witness is at step t^*=54 with occupancy 13, and the largest occupancy in 300 steps is 19. Guarded, the largest occupancy is 12. The guarded and unguarded traces share randomness until the guard first rejects an arrival, at step 20. At C=20 the seed-7 trace shows no violation in 300 steps, which raises the question of section 4.

Break it. Guard off, or C below n^*.

4. Proof, probability or a sample: three strengths of one claim

Idea. The same invariant can be argued three ways: a heuristic (the drift says trouble), statistical evidence (k of N sampled traces violate), and a proof or exact computation. Exhaustive methods explore "all possible states of the system" (krichen2023_e60e ↗, model checking). Sampling explores the states it happens to visit.

Exact value. For the unguarded chain, propagate the distribution over \{0,\ldots,C+1\} forward, with C+1 absorbing and binomial departures:

The binomial pmf is built by the recurrence \mathrm{pmf}(0)=(1-p_\ell)^n, \mathrm{pmf}(d+1)=\mathrm{pmf}(d)\,\frac{n-d}{d+1}\frac{p_\ell}{1-p_\ell}, in the workbook and in the widget alike. The shortest bad prefix is C+1 arrivals with no departure in between, of probability p_a^{C+1}(1-p_\ell)^{C(C+1)/2}.

Sampled value. From N traces, k violate. The Wilson 95% interval (with z=1.96) is

The corpus holds nothing on sampling against exhaustive evidence for rare violations, so treat the interval as standard statistics background.

Worked numbers. Exact probability of a violation within 300 steps, p_\ell=0.07:

At the widget default (C=20, p_a=0.9, N=200, seed 7) the sample gives 24 of 200, Wilson interval [0.0820,0.1723], and the exact value 0.1567 lies inside it. The shortest bad prefix is 21 steps, with probability 2.633\times10^{-8}. In the dense case (C=12, p_a=0.9) all 200 traces violate.

Break it. Press "rare bug" (C=20, p_a=0.5): 0 of 200 sampled, Wilson upper bound 1.96^2/(200+1.96^2)=0.0188, exact value 2.297\times10^{-5}, reachable by a 21-step prefix of probability 1.148\times10^{-13}. With N=10 the bound is 0.2775. The readout says: sampling found nothing, and the state is reachable.

In words: zero sampled violations bound the probability. They do not prove the state is unreachable. That is the case for the rest of the course.

5. Safety or liveness: can a finite prefix refute it?

Idea. The two definitions mirror each other. Safety: \sigma\notin P implies some prefix \sigma[0..k] has no extension in P. Liveness: every finite prefix has some extension in P. Checking safety needs only reachability; checking liveness needs to consider "nonterminating, infinite, executions" (alur1999_8e22 ↗, section "Tools"). Alpern and Schneider showed that every property is the intersection of a safety and a liveness property; the corpus does not hold that paper, so this is textbook background.

In words: a safety claim can be lost in finite time. A liveness claim can never be lost in finite time.

Worked verdicts (prefix k=40, deadline D=20). The prefix \sigma[0..k] has k+1 states. The visitor trace is ENTER, LOBBY, ROOM_A, ROOM_B, ROOM_A, ROOM_B, ...

"Exits within D" means \sigma_s=\mathrm{EXIT} for some s\le D, the same t_{\text{exit}}\le D as in section 8. The deadline is missed once the visitor is still inside at step D: the prefix \sigma[0..D], of length D+1, is a bad prefix.

6. Reachability as a fixpoint, and the lasso

Idea. The reachable set is the least fixpoint R=\{s_{\text{init}}\}\cup\mathrm{post}(R), computed as R_0\subseteq R_1\subseteq\cdots with R_0=\{s_{\text{init}}\} and R_{i+1}=R_i\cup\mathrm{post}(R_i), where \mathrm{post}(X)=\{s':\exists s\in X,\ s\rightarrow s'\}. Each round that changes R adds at least one state, and there are |S| states, so the computation stops after at most |S| rounds.

In words: keep adding one-step successors until nothing new appears.

Two questions come apart. "EXIT is reachable" means some run exits. "Every run reaches EXIT" is stronger, and fails on a lasso: a finite stem followed by a cycle repeated forever, never taking the exit. It also fails on a deadlock: a state of R\setminus\{\text{EXIT}\} with no successor, where a finite maximal run stops short. The lasso as a model checker's liveness counterexample is standard background; the one corpus passage that states it sits under a mis-indexed key, so it is not cited here.

Algorithm. Forward search gives R. For "every run reaches EXIT" compute the greatest fixpoint Z=\nu Z.\,(R\setminus\{\text{EXIT}\})\cap\mathrm{pre}(Z), the states from which some run avoids EXIT forever. A lasso exists from ENTER iff ENTER \in Z, and a depth-first walk inside Z extracts the stem and the cycle. The workbook names the functions reachable_fixpoint, lasso and deadlocks; weeks 3 and 5 reuse them.

Worked numbers. The visitor schedule has states ENTER, LOBBY, ROOM_A, ROOM_B, EXIT and edges ENTER→LOBBY, LOBBY→ROOM_A, ROOM_A→ROOM_B, ROOM_B→ROOM_A (the loop-back), ROOM_B→EXIT, EXIT→EXIT. Then R_2=\{\text{ENTER, LOBBY, ROOM\_A}\}, the fixpoint is reached after 4 growing rounds (round 5 adds nothing), |R|=5 of 5, EXIT is reachable, and not every run reaches EXIT: the lasso is ENTER, LOBBY, (ROOM_A, ROOM_B) repeated forever.

A second preset, a job dispatcher with states QUEUED, RUNNING, FAILED, DONE and a retry edge FAILED→RUNNING, has DONE reachable and a lasso QUEUED, (RUNNING, FAILED) forever. Delete the retry edge and FAILED becomes a dead end: a missing edge is a deadlock.

Break it. Click an edge to delete it. Deleting ROOM_B→EXIT drops EXIT out of R; deleting ROOM_B→ROOM_A makes every run reach EXIT; deleting ROOM_A→ROOM_B deadlocks ROOM_A.

7. "Almost surely" is not "surely"

Idea. Give each visitor an exit probability p per step. Then \Pr[\text{inside at }t]=(1-p)^t. For p=0.005 and t=500: 500\ln0.995=-2.506 and (0.995)^{500}=e^{-2.506}=0.0816.

In words: every visitor leaves eventually, but at no finite time can you prove that everyone has. Liveness holds with probability 1, since (1-p)^t\to0, yet a skeptic watching the building cannot tell "will leave, has not yet" from "will never leave". This previews the probabilistic week (week 10).

Worked numbers (widget default). p=0.005, t=500, N=200, seed 7: theory 8.16% remain, about 16.3 visitors of 200; the sample shows 13 of 200, 6.5%. At t=1000 theory gives 0.0067 and the sample 2 of 200; at t=2000 theory gives 4.4\times10^{-5} and the sample 0 of 200. The sample is built from one generator stream, visitor by visitor, run to a fixed horizon of 2000 steps, so moving the horizon slider does not change it.

Break it. Set p=0: the curve stays at 1.0 forever, 200 of 200 remain at t=500. That is the lasso of section 6 seen statistically, and "eventually" is now false, not merely unproven.

8. Bounded liveness is safety: buy back a finite witness with a deadline

Idea. Strengthen "eventually exits" to "exits within D steps". Any violation now has a finite bad prefix: a visitor still inside at step D, that is \sigma[0..D] of length D+1. So \varphi_D:\ \forall a\ t_{\text{exit}}(a)\le D is a safety property, and the lasso has become a bad prefix. Tools check such properties natively: UPPAAL "allows checking of safety and bounded liveness properties" (alur1999_8e22 ↗, section "Tools"), and the same paper writes bounded response in a real-time temporal logic (a request followed by a response within a stated number of time units). Queries appear as A[] not deadlock, A<> ... and E<> ... (houimli2017_4680 ↗, section IV.B).

The bound. A timeout guard forces the exit once a dwell would end after T_{\text{guard}}: from t=0, draw a dwell d=5+\lfloor u\,(d_{\max}-4)\rfloor; if t+d>T_{\text{guard}} the visitor exits at t+d, otherwise t\leftarrow t+d. Then t\le T_{\text{guard}} before the last dwell, so

In words: naming a deadline turns an infinite counterexample into a finite one. The price is a validation question: is D acceptable in the world? The mathematics cannot choose D; it can only tell you whether a guard makes a chosen D true by construction.

Worked numbers (widget default). T_{\text{guard}}=120, d_{\max}=30 (minimum dwell 5, mean 17.5), N=200, seed 7: exits lie between step 121 and step 149, the latest is 149, inside the bound 150. With D=150 no visitor exceeds D, and the readout says the property holds by construction.

![Exit steps of 200 visitors under the timeout guard: all inside (120, 150], latest 149.](fig_w1_deadline.png)

Break it. Set D=140 (below the bound): 27 of 200 sampled visitors break it, the first is visitor number 3, exiting at step 141 and so still inside at step 140. Or switch the guard off: no visitor exits within the horizon of 500 steps, and the very first visitor gives a bad prefix of length D+1=151.

9. Classify it: the counterexample tells you the class

Idea. Every requirement is classified by the shape of its counterexample: a bad prefix (safety), a lasso (liveness), or a deadline miss (bounded liveness, which is safety). If you can draw the counterexample, you know which checker you need: a reachability search for a bad prefix, a cycle search for a lasso. The widget's eight requirements have three safety, three liveness and two bounded items; the default is item 3, the pump that shuts off within 5 s of a leak signal, answered "bounded" (score 1 of 8).

Concept check. Classify each and give the counterexample shape: (a) "the two inertial units never disagree by more than 1 degree"; (b) "every request is eventually acknowledged"; (c) "every request is acknowledged within 200 ms"; (d) "the mutex is never held by two tasks". (a) safety, one finite trace showing a disagreement. (b) liveness, a lasso with a request on the stem and no acknowledgement on the cycle. (c) bounded liveness, hence safety: a request followed by 200 ms of silence. (d) safety, a finite trace ending with both tasks holding it.

Two failures from engineering history (background, not in the corpus). Ariane 5: an unprotected conversion of a 64-bit value to a 16-bit integer, whose range argument held for the predecessor's trajectory; the code was reused and the assumption did not travel with it. Therac-25: an interlock obligation that once lived in hardware moved to software, where nobody stated it as a property. Neither is in the corpus, and no figures are quoted because none traces to a source we hold. Sources: Lions et al. (1996), the Ariane 5 inquiry report; Leveson and Turner (1993).

Concept check. "The converted value always fits in 16 bits" was proved for the predecessor's trajectory and failed on the new one. In the verification and validation vocabulary of section 1, which failure is that? (A validation failure of an assumption. The verification was sound for the stated environment model; the environment model no longer matched reality, and the verification was never re-run.)

Exam-style questions

Q1 (classification). Classify each requirement as safety, liveness or bounded liveness, and describe the exact shape of a counterexample: (a) "no two trains ever occupy the same track segment"; (b) "every buffered message is eventually delivered"; (c) "the pump shuts off within 5 s of a leak signal"; (d) "the counter never decreases".

Model answer. (a) Safety; a finite trace ending in a state with two trains on one segment. (b) Liveness; a lasso whose stem buffers a message and whose cycle never delivers it. (c) Bounded liveness, hence safety; a finite trace with a leak signal followed by 5 s without shut-off. (d) Safety; a finite trace containing one decreasing step. Full marks need the shapes, not only the labels.

Q2 (drift). A queue admits one job per step with probability 0.6; each queued job completes with probability 0.05 per step. The requirement is "the queue never exceeds 10". Derive the drift, find its zero, and predict whether the invariant survives. What single change to the transition relation enforces it by construction?

Model answer. d(n)=0.6-0.05n and n^*=12>10, so the process hovers above the cap and the invariant fails almost surely. Guard: reject an admission when n=10. By induction the reachable states are \{0,\ldots,10\} and the invariant holds by construction.

Q3 (reachability and lassos). A graph has edges ENTER→A, A→B, B→A, B→C, C→C, initial state ENTER and goal C. Compute the reachable set, say whether "eventually C" can be violated, and if so exhibit the lasso.

Model answer. R=\{\text{ENTER, A, B, C}\}, so C is reachable. Yet "eventually C" is violated by the lasso with stem ENTER→A and cycle A→B→A, which never takes B→C. Reachability of the goal is necessary but not sufficient for liveness. Which of these lassos count as legitimate runs is a question the linear-time and branching-time weeks (LTL, week 4; CTL, week 5) settle with their own semantics.

Q4 (bounded liveness is safety). Prove from the definitions that "every visitor exits within 150 steps" is a safety property, and say what is gained and what must now be defended.

Model answer. Any violating trace has a visitor still inside at step 150. The prefix up to that step is a bad prefix: no extension repairs it, since the deadline has passed. So every violation has a finite bad prefix, which is the safety definition. Gained: finite refutability, so the property can be monitored at run time and checked by state exploration. To defend: the value 150, a validation question about the world and not a theorem.

Q5 (validation). A model of a room with an admission guard is proved never to exceed 12 people. The real room has an unguarded side door. State what the proof shows and does not show, exhibit a world trace that violates the requirement, and name the cheapest way to close the gap.

Model answer. It shows \mathrm{Traces}(\mathcal T_{\text{model}})\subseteq P and nothing about the world. From occupancy 12 the guard rejects the main-door arrival, but a side-door arrival with no departure gives 13 (in the widget, seed 7, side-door probability 0.10, the world first crosses at step 31). The cheapest closure is to add the side door to the model, after which the property fails and the counterexample is informative; or to guard the door. Whether the model now matches the room is a validation question, closed by observation and not by proof.

Q6 (evidence). With C=20, p_a=0.5, p_\ell=0.07, 200 sampled traces of 300 steps show no violation. What may you claim, what may you not, and what settles the question?

Model answer. You may claim that no violation was found in 200 traces, and that the probability of a violation is below 0.0188 at 95% (Wilson upper bound). You may not claim the state is unreachable: it is reachable by a 21-step prefix, and the exact probability is 2.297\times10^{-5}. An exact computation or an exhaustive exploration settles it; a larger sample only lowers the bound.

Further reading

• alur1999_8e22 ↗: safety by reachability, liveness by infinite executions, and UPPAAL's safety and bounded-liveness checking; the entry point to weeks 4, 5 and 9.
• wedyan2017_50ae ↗: a model checker verifies a system description against a specification; anchors the verification and validation distinction of section 1.
• abrial2010_b911 ↗: modelling as the elimination of specification gaps, and the static checker as the well-formedness gate (section 2).
• krichen2023_e60e ↗: model checking explores all states; early defect discovery. Supports the case for exhaustive methods in section 4.
• houimli2017_4680 ↗: reachability, liveness and deadlock queries as a tool writes them (section 8).
• murata1989_d3ec ↗: boundedness as a finite reachable set, detected by the coverability tree, and safeness as "absence of overflows"; the guard's cousin in week 6.
• hoferschmitz2020_1b73 ↗: further reading only; the course anchor for week 1. No passage read for this note supports a specific claim here.
• Textbook background, not in the corpus: Alpern and Schneider (1985), Defining Liveness; Lamport (1977), Proving the Correctness of Multiprocess Programs; Baier and Katoen, Principles of Model Checking; Leveson and Turner (1993), the Therac-25 investigation; Lions et al. (1996), the Ariane 5 inquiry report. The corpus is silent on these; nothing above is quoted from them.

Where this goes: week 2 (logic) takes the schema as a propositional constraint and the property statements as formulas; week 3 (transition systems) reuses the fixpoint and adds counterexample paths and state counts; week 4 (LTL) writes \mathbf G(\mathrm{occ}\le C), \mathbf F\,\mathrm{EXIT} and a bounded response; week 5 (CTL) reads section 6's two questions as EF against AF; week 6 (Petri nets) generalises the guard's boundedness; week 9 (timed automata) makes deadlines first-class; week 10 (probabilistic models) makes "almost surely" precise.

Provenance (instructor only)

No first-party measurement appears in this note. Every number comes from the toy models in workbook.ipynb; the labels are in numbers.json.

• obsidian/monad-knowledge/edu/courses/FM505-formal-modelling-verification/week-01-from-informal-spec-to-checkable/workbook.ipynb
• obsidian/monad-knowledge/edu/courses/FM505-formal-modelling-verification/week-01-from-informal-spec-to-checkable/numbers.json
• obsidian/monad-knowledge/edu/courses/FM505-formal-modelling-verification/week-01-from-informal-spec-to-checkable/components/fm.mjs (the widget mirror of the workbook kernel)
• obsidian/monad-knowledge/edu/courses/WS501-wifi-csi-sensing/week-01-the-wireless-channel-how-a/components/math.mjs (the shared generator and widget pattern)
• superseded revisions of this folder's lecture.md, slides.md and workbook.ipynb (material carried over: the schema toy, the occupancy model and drift, the survival derivation, the 120 + 30 = 150 bound, concept checks and exam questions Q1 to Q4)