Testing cannot try everything
A game has two players who can each grab the last ticket in the same instant. You test it a thousand times and it works. The bug needs one exact order of events, and it shows up in the thousand and first. A formal method does not try cases. It asks a machine to look at all of them.
By the end of this lesson
Note
I can say what a solver and a model checker give back when a property is false.
Key words
- Property: a statement about a system that should always be true.
- Solver: a program that finds values that fit a set of rules.
- Model checker: a program that tries every state a model can reach.
- Invariant: a property that must hold in every state.
- Counterexample: a run that shows the property is false.
- Model: a small description of a system that leaves out the detail.
Starter: what you already know
Note
Answer in your head. 1. What is a variable? 2. What is a condition in an if? 3. What can go wrong when two programs change the same thing at once? You need the third answer in a moment.
Before you start
Note
Press Start the lab on the bar at the top of this lesson. This lab is a whole Ubuntu machine of your own, so it takes a little longer to come up than a container. Each Run button types its command into the machine's terminal, one after another in the same session. If one says the machine is still starting, wait a few seconds and press it again. The first run of a Java tool takes a few seconds. To watch them, or to type your own, press Open terminal on the bar.
A solver finds values, or proves there are none
Z3 is a solver. You give it rules and it answers sat (satisfiable: some values fit) with an example, or unsat (no values fit). The first command shows the version. The second asks for a number x above 3 and below 6: Z3 says sat and gives x as 4. The third asks for one above 5 and below 3: Z3 says unsat. That is how it proves things: to prove a claim, ask for a case where it fails and get unsat.
z3 --versionShown here, not run. Create a free account to press Run and type it into your own lab’s terminal.
echo '(declare-const x Int) (assert (and (> x 3) (< x 6))) (check-sat) (get-model)' | z3 -inShown here, not run. Create a free account to press Run and type it into your own lab’s terminal.
echo '(declare-const x Int) (assert (and (> x 5) (< x 3))) (check-sat)' | z3 -inShown here, not run. Create a free account to press Run and type it into your own lab’s terminal.
Check
Tip
Z3 says unsat for rules about a timetable. Has it found a timetable? Answer: no. unsat means no timetable obeys all the rules, so the rules contradict each other.
A model checker finds the bad order
SPIN checks models written in Promela. Your lab has one: two workers add 1 to a shared counter, and a lock that does nothing yet. spinrun builds the checker and runs it over every order the workers can take. It prints assertion violated (inside==1) and errors: 1, and keeps a trace. The second command replays that trace step by step: both workers did inside = (inside+1) before either one left.
spinrun formal/spin/main.pmlShown here, not run. Create a free account to press Run and type it into your own lab’s terminal.
spin -t -p formal/spin/main.pmlShown here, not run. Create a free account to press Run and type it into your own lab’s terminal.
A common mistake
Warning
Many people think a model checker proves a program is correct. It proves the model has the property you wrote down, and nothing more. An invariant of TRUE is never broken, so a checker passes it at once and tells you nothing. The property has to say something a broken system would fail.
An invariant can be false of a good system
TLA+ describes a system as states and steps, and TLC checks it. The lab's Lock.tla has two processes that can each be idle, wait or cs (in the critical section). This invariant says they are never both waiting. That is false even of a correct lock, and TLC prints Invariant NotBothWaiting is violated and a counterexample of three states, ending with both processes at wait. The lab's real task is a different invariant.
tlc formal/tla/Lock NotBothWaitingShown here, not run. Create a free account to press Run and type it into your own lab’s terminal.
A counterexample can be a picture of people
Alloy describes things and the links between them, then looks for a small example that breaks a claim. Here the things are people and who is whose friend. alloy runs both commands in the file. check Symmetric prints SAT: Alloy found a counterexample, two people where one counts the other as a friend and not the other way round, shown as Person$1->Person$0. run Meet prints SAT too: it found an example to look at. For a check, SAT means the claim is broken.
alloy formal/alloy/model.alsShown here, not run. Create a free account to press Run and type it into your own lab’s terminal.
Now do the lab
Tip
You have seen a solver, a trace, a counterexample and an instance. Your lab asks you to write the rules, the lock, the invariant and the repair, and then each tool checks them. Open the README.md in your home folder with cat README.md in the terminal.
Exit check
Tip
Answer without looking back. 1. What does Z3 say when no values fit the rules? 2. What is a counterexample? 3. What is wrong with an invariant of TRUE? 4. For an Alloy check, what does SAT mean? Answers: unsat; a run that shows the property is false; it is never broken, so it proves nothing; a counterexample was found.
For teachers
Tip
This lesson is a small example of a lesson worked in a lab: the steps and the Run buttons are the lesson, and the lab is each student's own copy. This lesson is worked in a VM lab: each student has an Ubuntu machine of their own with four verification tools, and a Run types into its terminal and shows what it printed. Key learning points: 1. A solver answers sat with an example or unsat with none. 2. A model checker tries every order of events and gives a counterexample when a property fails. 3. An invariant of TRUE proves nothing. 4. A counterexample is the tool's evidence, and it can show that the property was the wrong one. Common mistake: believing a pass means the system is correct. Equipment: the lab and a browser; TLC and Alloy need a signed-in VM, which can reach GitHub. Tip: before spinrun, ask the class to find the bad order by hand. The lab itself has a check that runs each tool. Copy it into your own module and change it, or build one from scratch with the Lab menu in the lesson builder.