Bounded model checking of invariants

In cases where either the set of reachable states is infinite, or it is finite but too large to be explored in reasonable time due to time and memory limitations, bounded model checking is an appealing formal analysis method. The idea of bounded model checking is that we model check a property, not for all reachable states, but only for those states reachable within a certain depth bound, that is, reachable by a sequence of transitions of bounded length. Of course, our analysis is not complete anymore, since we may fail to find a counterexample lying at greater depth. However, bounded model checking can be quite effective in finding counterexamples and it is a widely used procedure. Bounded model checking of invariants is supported in Maude by means of the bounded search command.

Consider the following specification of a readers-writers system.

  mod READERS-WRITERS is 
    sort Nat .
    op 0 : -> Nat [ctor] .
    op s : Nat -> Nat [ctor] .
    
    sort Config .
    op <_,_> : Nat Nat -> Config [ctor] .  --- readers/writers

    vars R W : Nat .

    rl < 0, 0 > => < 0, s(0) > .
    rl < R, s(W) > => < R, W > .
    rl < R, 0 > => < s(R), 0 > .
    rl < s(R), W > => < R, W > .
  endm

A state is represented by a tuple < R, W > indicating the number R of readers and the number W of writers accessing a critical resource. Readers and writers can leave the resource at any time, but writers can only gain access to it if nobody else is using it, and readers only if there are no writers.

Taking < 0, 0 > as the initial state, this simple system satisfies two important invariants, namely:

• mutual exclusion: readers and writers never access the resource simultaneously: only readers or only writers can do so at any given time.
• one writer: at most one writer will be able to access the resource at any given time.

We could try model checking these two invariants in two different ways:

• we can represent the invariants implicitly by representing their negations through patterns; or
• we can represent them explicitly as Boolean predicates.

To model check our two invariants using an implicit representation we could use the commands

  Maude> search < 0, 0 > =>* < s(N:Nat), s(M:Nat) > .

  Maude> search < 0, 0 > =>* < N:Nat, s(s(M:Nat)) > .

since the negation of the first invariant corresponds to the simultaneous presence of both readers and writers, which is exactly captured by the first pattern < s(N:Nat), s(M:Nat) >; whereas the negation of the fact that zero or at most one writer should be present at any given time is exactly captured by the second pattern < N:Nat, s(s(M:Nat)) >.

The problem with the above two search comands is that, since the number or readers allowed is unbounded, the set of reachable states is infinite and the commands never terminate. We can instead perform bounded model checking of these two invariants by giving a depth bound, for example $10^{5}$, with the commands:

  Maude> search [1, 100000] in READERS-WRITERS : 
           < 0, 0 > =>* < s(N:Nat), s(M:Nat) > .
  
  No solution.
  states: 100002  rewrites: 200001 in 312460ms cpu (636669ms real) 
    (640 rews/sec)

  Maude> search [1, 100000] in READERS-WRITERS : 
           < 0, 0 > =>* < N:Nat, s(s(M:Nat)) > .
           
  No solution.
  states: 100002  rewrites: 200001 in 70600ms cpu (623434ms real) 
    (2832 rews/sec)

As the reader can observe, these computations take quite a long time. Notice that the terms appearing during the search grow very quickly. A very simple way of improving performance in this case is using the iter attribute for the s operator.

    op s : Nat -> Nat [ctor iter] .

Then, we obtain a much better performance:

  Maude> search [1, 100000] in READERS-WRITERS : 
           < 0, 0 > =>* < s(N:Nat), s(M:Nat) > .

  No solution.
  states: 100002  rewrites: 200001 in 610ms cpu (1298ms real) 
    (327870 rews/sec)

  Maude> search [1, 100000] in READERS-WRITERS : 
           < 0, 0 > =>* < N:Nat, s(s(M:Nat)) > .

  No solution.
  states: 100002  rewrites: 200001 in 400ms cpu (1191ms real) 
    (500002 rews/sec)

In the following section we will use some formal tools for checking properties about the READERS-WRITERS module. Since some of these tools cannot handle the iter attribute, we use the module as shown above.