	Model Checking @CMU

[Home]

[People]

[Software]

[Publications]

[Support]

[Links]

[Internal]

Model Checking Guided tour

This page gives a quick overview of how the SMV model checking system is used. A simple example is presented, and its analysis performed. The example is extremely simple, and the analysis superficial for brevity. This demo just shows how the tool is used, and by no means indicates the size of problems that can be handled. The actual installation of SMV is quite simple, and we encourage you to try the real code.

The complete tour takes about 5 pages.

An SMV program may consist of several modules. Each module is an encapsulated description that may be instantiated several times within the model. For example, the declaration

MODULE proc(state0, state1, turn, turn0)

defines proc as a module with 4 formal parameters.

Within every module, local variables may be declared. The type of a variable may be boolean, an enumeration type or an integer subrange.

VAR state0: {noncritical, trying, critical, ready};

Modules are also instantiated using variable declarations. A module may contain instances of other modules, allowing a structural hierarchy to be built. For example, the module main declares the variable p0 as an instance of proc

VAR p0: proc(s0, s1, turn, 0);

Every SMV description has to contain a module called main, with no formal parameters. This module forms the root of the model hierarchy and the starting point for building the finite-state model for a given description.

The value of the variables in each state are defined using init and next:

init(state0) := noncritical;
next(state0) := case
  (state0 = noncritical): {trying, noncritical};
  (state0 = trying) & ((state1 = noncritical) | (state1 = trying)): ready;
  ...
esac;

The code above defines the initial value of state0 to be noncritical, and the value of that variable in the next state as a function of the value of the variables in the current state. Notice that if state0 is noncritical, then in the next state its value could be trying or noncritical, and the choice is made nondeterministically.

This presentation briefly shows how to describe a system to be verified in the SMV language. Several features have been omitted for brevity. The reader is referred to the SMV manual for a more complete description.

The code for the example is presented below. It is a simple mutual exclusion algorithm for two processes:

MODULE main
VAR
  s0: {noncritical, trying, critical, ready};
  s1: {noncritical, trying, critical, ready};
  turn: boolean;
  pr0: process prc(s0, s1, turn, 0);
  pr1: process prc(s1, s0, turn, 1);

The variables s0 and s1 correspond to the state of each process. turn is used to guarantee that no starvation occurs. The processes are then instantiated using the process keyword. This makes the processes execute asynchronously, that is, at each step only one executes, and the choice is nondeterministic.

ASSIGN init(turn) := 0;

FAIRNESS !(s0 = critical)
FAIRNESS !(s1 = critical)

The initial value of turn is set to false. The fairness constraint FAIRNESS p indicates that only paths in which p happens infinitely often will be traversed. In this example the constraint states that both processes cannot stay in the critical region indefinitely.

MODULE prc(state0, state1, turn, turn0)

ASSIGN
init(state0) := noncritical;
next(state0) := 
case
   (state0 = noncritical) : {trying,noncritical};
   (state0 = trying) & ((state1 = noncritical) | (state1 = trying) |
                        (state1 = ready)): ready;
   (state0 = ready): critical;
   (state0 = trying) & (state1 = trying) & (turn = turn0):  critical;
   (state0 = critical) : {critical,noncritical};
   1: state0;
esac;

next(turn) :=
case
   turn = turn0 & state0 = critical: !turn;
   1: turn;
esac;
FAIRNESS running

The code above defines the value of the process state during the execution. If the process is in the noncritical state, it can request mutual exclusion at any point (chosen nondeterministically), by going to the trying state. Once the conditions for mutual exclusion are satisfied it goes to the ready state, and enters the critical region one step later. In the critical region, the process can decide to go to the noncritical region at any point. Finally, the value of the turn variable is updated to avoid starvation. This completes the code for the example. We will now see how specifications are written, and the results of the verification.

Mutual exclusion is specified by the following temporal logic formulas:

SPEC AG((s0 = critical) -> !(s1 = critical))
SPEC AG((s1 = critical) -> !(s0 = critical))

AG p means that in all possible execution sequences (specified by the A part), it is globally true (the G part) that p holds. In other words, p is invariant. In this case we are saying that once a process is in the critical region, the other process cannot be in its critical region.

SPEC AG((s0 = trying) -> AF(s0 = critical))
SPEC AG((s1 = trying) -> AF(s1 = critical))

Another useful property is expressed by the formulas above. They state that an invariant of the model is the fact that if a process is in the trying region, then in all possible execution sequences, at some point in the future (indicated by the F part), it will be in the critical region. In other words, a request for mutual exclusion will always be granted.

However, the model above is not correct! SMV was able to determine that mutual exclusion is violated, and to produce a counterexample to show why this happens (only one counterexample is shown here):

-- specification AG (s0 = critical -> !s1 = critical) is false -- as demonstrated by the following execution sequence state 1.1: s0 = noncritical s1 = noncritical turn = 0 state 1.2: [executing process pr1] state 1.3: [executing process pr1] s1 = trying state 1.4: [executing process pr0] s1 = ready state 1.5: [executing process pr0] s0 = trying state 1.6: [executing process pr1] s0 = ready state 1.7: [executing process pr0] s1 = critical state 1.8: s0 = critical

It shows that both processes can enter the critical region at the same time, if the sequence of events showed occurs.

In more realistic situations, we would proceed and try to debug the problem. However, this is out of the scope of this demonstration, and we leave solution of this error as an exercise for the reader...
And you can do it now! (online smv-trial is broken currently!)

Finally, after completing the verification, SMV outputs usage information:

resources used: user time: 0.1 s, system time: 0.09 s BDD nodes allocated: 3160 Bytes allocated: 917504 BDD nodes representing transition relation: 54 + 1 reachable states: 32 (2^5) out of 32 (2^5)

This example is verified almost instantaneously, as can be seen above. More interesting usage information can be seen below. This has been produced by a real example verified by our group:

resources used: user time: 4251.28 s, system time: 0.03 s BDD nodes allocated: 1114179 Bytes allocated: 18808832 BDD nodes representing transition relation: 135481 + 23982 reachable states: 1.245e+07 (2^23.5696) out of 4.06368e+28 (2^95.0368)

CMU-SCS Model Checking home page

Please send any comments and suggestions to Nishant Sinha - (nishants) at cs dot cmu dot edu.