Programs with Proofs: Model-Checking Example with Spin

Method of Proving

This is a program written in Promela, a language for writing models of concurrent systems. The Promela models can be verified to follow certain properties by a model-checking tool called Spin. The properties which can be verified include system invariants, assertions, absence of deadlocks and non-progress cycles, Linear Temporal Logic (LTL) formulae etc.

This manual provides a good starting point to learn Promela language and usage of Spin. The syntax for specifying LTL formulae is described here. For a collection of other useful links, refer this page.

In contrast to predicates which are true or false based on the current state, the LTL formulae allow us to express properties about a sequence of states. For example, we can express that a certain property P will hold at least once in some future state, or that property Q must hold in all states until a state satisfying R is reached.

This is an example program focusing on how to specify LTL formulae and assertions. It has been proved using Spin 6.4.9, on an x86_64 system running Debian 10 Linux. To prove the properties specified for this program, we may use below commands (use "spin --" for the complete list of options):

spin -a filename (this generates file "pan.c" and others)
gcc -o pan pan.c
Now we can prove each of the LTL formulae one by one using its name (use "./pan --" for the complete list of options), for example:
./pan -a -N p1

For each command in step (3) above, we should see "errors: 0" in an output line like below:
State-vector ... byte, depth reached ..., errors: 0

This would also mean that the assertion has been proved.

An Example


/* A Promela model with two processes "sender" and "receiver", where the
   sender sends 100 messages to be received and processed by the receiver.
   Refer to the comments accompanying the code below. */

mtype = {msg};

/* a channel with buffer for 10 messages */
chan c = [10] of {mtype, int};

/* all the globals below are automatically initialized to 0 */

/* counters */
int sent, received, processed;

/* value of "i*i"; i is the latest even value received in messages */
int isqr;

/* LTL formulae to specify various properties about the global variables */

/* Valid range of variables sent, received and processed (in all states) */
ltl p1 {[] (0 <= sent && sent <= 100 &&
            0 <= received && received <= sent &&
            0 <= processed && processed <= received/2)}

/* Since isqr is the square of an even "i", it must be a multiple of 4
   (in all states) */
ltl p2 {[] (isqr%4 == 0)}

/* In any state with (processed >= 10), (isqr >= 400) must hold */
ltl p3 {[] ((processed >= 10) -> (isqr >= 400))}

/* Some state must be reached with (isqr == 900) ("i" becomes 30) */
ltl p4 {<> (isqr == 900)}

/* Some state must be reached with (isqr == 64), and till then (sent < 20)
   must hold */
ltl p5 {(sent < 20) U (isqr == 64)}

/* After a state with (sent >= 50), some state must be reached with
   (processed >= 25) */
ltl p6 {[] ((sent >= 50) -> <>(processed >= 25))}

/* After a state with (sent == 100), some state must be reached with
   (received == 100) and (processed == 50) */
ltl p7 {[] ((sent == 100) -> <>(received == 100 && processed == 50))}


/* The sender process */
active proctype sender()
{
  /* Send 100 messages with "int" field from 1 to 100. Note that the
     channel c can buffer only upto 10 messages at a time, so waiting
     may happen. */

  do
    :: sent < 100 ->
        atomic {c!msg(sent+1); sent++;}

    :: else       ->
        break;
  od
}

/* The receiver process */
active proctype receiver()
{
  int i;

  /* Receive each of the 100 messages, while tracking the count in
     "received". Whenever the channel is empty, waiting will happen.
     The messages with even value "i" in the "int" field are "processed"
     by updating "isqr" to "i*i". */

  do
    :: received < 100 ->
        c?msg(i);

        /* example of an assertion */
        assert(i >= 1 && i <= 100);

        received++;

        if
          :: i%2 == 0 -> isqr = i*i; processed++;
          :: else
        fi

    :: else           ->
        break;
  od
}