6. Model Checking
Todo
Under construction for spring 2025
For an overview, please review these resources:
In addition, various TLA+ examples are available here:
6.1. Use case: finding a solution to a puzzle
In these use cases, we use model checking to falsify an invariant corresponding to the absence of a solution. If there is a solution, the model checker finds one.
Examples:
6.2. Use case: verifying an interactive, event-based system
In these use cases, we use model checking to verify safety and liveness properties of event-based systems. These systems typically respond to external and internal stimuli (events), such as pressing a button, inserting a coin, an internal timer counting down, etc. In response to these events, the systems undergo state changes.
As an example of a safety property from the user’s (consumer’s) point of view, a microwave oven should not allow radiation to occur with the door open. As an example of a liveness property, once the microwave oven is running, it should stop running within a finite amount of time.
Examples:
6.3. Use case: checking the thread safety of a concurrent system with explicit threads
In these use cases, we model threads explicitly as finite state machines based on the underlying control flow graph.
Examples:
Data structure shared among multiple concurrent clients (TODO)
These references contain more background material on concurrency in general and the extent of nondeterminism resulting from concurrent activities in a system, which can quickly become unwieldy even with a small number of concurrent threads.
6.4. Extended example: ticket vending machine
The objective is to write and check a TLA+ specification for a ticket vending machine that sells one-way train tickets to several known destinations.
We’ll make some simplifying assumptions: All tickets to the same destination have the same fare, but the fare may vary across destinations. The machine is initially loaded with zero or more tickets for each known destination, and zero or more coins in its internal bank.
When in operation, the machine responds to the following external actions:
Passenger deposits a coin.
Passenger selects a destination. If they have deposited enough coins, the corresponding ticket is delivered, the money needed to pay for it is retained by the machine, and any amount of extra money they may have deposited is returned to them (the machine gives change.) Otherwise, nothing happens.
Passenger selects “cancel.” Any coins they have deposited so far are returned.
Your specification should allow you to use TLC to check the property that the total value of tickets still in the machine plus money in its internal bank is invariant during operation. Actually, this isn’t quite true: you’ll need to come up with a more precise invariant that is true.
For simplicity, assume that tickets all cost some multiple of $1, and the machine only accepts dollar coins.
6.4.1. Additional thoughts
The set of destinations and their fares should be CONSTANTS. Represent destinations as a set of model values. Represent fares as a function from destinations to Nat (you’ll need to make your spec EXTEND Naturals). Hint: to describe a concrete function given by the ordered pairs {(d1, r1),(d2, r2), … ,(dn, rn)} as the value of a constant, use the notation ( d1 :> r1 @@ d2 :> r2 @@ … @@ dn :> rn ).
The VARIABLES should include the currently available tickets (a function from destinations to Nat), the current internal bank (a Nat for each kind of coin), and the amount deposited so far (again, a Nat for each kind of coin).
The initial values of these variables should be specified as CONSTANTS too (except for the coins deposited so far, which can be initialized to zero).
There should be three actions; the Next action should just be a disjunction of these.
You may find the following higher-order operator (familiar from functional languages) useful for computing the value of the tickets in the machine:
(* Operator to fold over a set s using function f and initial value i *)
Fold(f(_,_),i,s) ==
LET DFold [s0 \in SUBSET s] ==
LET elt == CHOOSE e \in s0 : TRUE IN
IF s0 = {} THEN i ELSE f(elt, DFold[s0 \{elt}])
IN
DFold[s]
(* Example: compute sum of a set *)
Sum(s) == Fold(LAMBDA e,r : e + r,0,s)
See also this reference for more ideas to consider and discuss.
6.5. Exercises
- Learning Objectives
An understanding of
event-driven systems
state diagrams
modeling event-driven systems with TLA+
- Description
The goal is to model a river crossing puzzle as an event-driven system using TLA+.
You may work on the wolf, goat, and cabbage puzzle, or another puzzle from this page, or you can suggest some other, similar puzzle.
- Submission
Each individual student who participated in the activity should submit a screenshot of their work completed by the end of the session.
- Learning Objectives
An understanding of
concurrent systems
bounded buffers with multiple producers and consumers (MPMC)
- Description
The goal is to model a system with a single, shared bounded buffer and multiple producers and consumers.
The producers are workstations submitting print jobs to the shared print queue (buffer).
The consumers are printers removing print jobs from the shared print queue.
The shared print queue is a fixed-size, circular, array-based buffer as described in this lab.
For now, we’ll hard-code the number of instances of producers and consumers, respectively.
We will also define the number of jobs each workstation submits to range over various values so that we’ll get many combinations.
Finally, we’ll define suitable temporal properties, e.g.
termination: the print queue should eventually be empty
eventual consistency: at the end, the total job count should be equal to the sum of the initial number of jobs each workstation was going to submit
- Submission
Each individual student who participated in the activity should submit a screenshot of their work completed by the end of the session.
A nice collection of model-checking exercises is available here.