“Model checking” (MC) seems like a very intimidating thing — which I only realized after I tried to explain it to a totally non-PL/FV person and failed. Afterwards, I searched “what is model checker” on Google, the returned results are not really satisfying — a bunch of lengthy and outdated slides and papers that people can’t quickly follow, learn, and take home. Thus I decided to write a small essay teaching you what is Model Checking and how it is useful.

Word by word, first, what is “model”? It is actually a formal way to specify the system requirements i.e. what the system (implementation) should do. And this is awesome: with MC, it is possible to figure out whether the system design document has any flaws, before putting it into development (yes, this separation of design and development is still what some people do today for critical systems, a.k.a. waterfall — However, most of the production code today is produced with an iterative workflow, like agile, which throws away the concept of having a flawless design document upfront). Here is the key — model checking verifies requirements, rather than implementation. In a lot of cases, model is just a state-transition system. Below is the example of a model and the all reachable states. Note that this example is actually a concurrent program. You will tell yourself — oh, isn’t that an implementation rather than requirements? The fact is that, program needs to be compiled and executed on a computer. In that sense, program can be viewed as a specification of what kind of computer state (memory + register + program counter) transitions are possible when running the compiled binary. State exploration is the process of turning a requirements/model into a state transition graph. Here, we use a simple concurrent interpreter as the underlying computer, when given one of the entry state (PC1 = 10, PC2 = 20, t = 0), we can execute either thread. If we execute thread 1, then we need to update PC1 from 10 to 11, since this is the semantic of white (true). Thus we add an edge from (PC1 = 10, PC2 = 20, t = 0) to (PC1 = 11, PC2 = 20, t = 0). You can produce the entire graph by following the normal program semantics combined with non-deterministic interleaving semantic (which means that you can choose to update either PC at any given state).

Second, what is “checking” — or, what to check? We want to check whether some specification is satisfied for such model. And the specification is normally written in a temporal logic language (this fancy language has primitives like “eventually” and “always”). Some of the properties include whether the system will deadlock, whether the output is correct upon termination etc. In the above example, the specification is about mutual exclusion, that two threads can be in the critical section (program point 12 and program point 22, correspondingly) at the same time, which can be written formally as:

always(not(PC1 == 12 and PC2 == 22))

After introducing the two concepts, you might wonder, how does a model checker work? Essentially, the process of model checking is an exhaustive exploration of the state space of a system, typically to see if an error state is reachable. If so, it produces concrete counter-examples. So here we need two things: one is an executor, that when given the model (state transition rules) and entry states, output all reachable states; another thing is a verifier, that when given the predicates and any state along with the path from some entry state to this state, check whether the predicate is satisfied, and if not, output this state and path as a counter-example.

How is MC useful? In real world, MC is applied in verifying the design of a lot of systems, both hardware and software.

  1. Richard Raimi used Motorola’s Verdict model checker to debug a hardware laboratory failure [3].
  2. SLAM [2] is used to verify the drivers in Windows operation system.
  3. TLA+ is a model checker used to validate the distribute protocols like Byzantine Paxos [1]

References

  1. Cousineau, Denis; Doligez, Damien; Lamport, Leslie; Merz, Stephan; Ricketts, Daniel; Vanzetto, Hernán (1 January 2012). TLA+Proofs (PDF). FM 2012: Formal Methods. Lecture Notes in Computer Science. 7436. Springer Berlin Heidelberg. pp. 147–154. doi:10.1007/978-3-642-32759-9_14. ISBN 978-3-642-32758-2. Retrieved 14 May 2015.
  2. https://www.microsoft.com/en-us/research/project/slam/
  3. http://www.cs.cmu.edu/~emc/15-398/lectures/overview.pdf
  4. https://en.wikipedia.org/wiki/TLA%2B#Model_checker
  5. https://en.wikipedia.org/wiki/Model_checking
  6. https://www.embedded.com/design/prototyping-and-development/4024929/An-introduction-to-model-checking
  7. https://ieeexplore.ieee.org/document/6606751
  8. https://www.cs.colorado.edu/~bec/courses/csci5535-s09/slides/lecture02.6up.pdf