= (Σ,E,ϕ,R) specified in Maude as a system module, we can define an
invariant I, yielding a decidable set of states, by:
A rewrite theory, specified in Maude as a system module, provides an executable mathematical model of a concurrent system. We can use the Maude specification to simulate the concurrent system so specified. But we can do more. Under appropriate conditions we can check that our mathematical model satisfies some important properties, or obtain a useful counterexample showing that the property in question is violated. This kind of model-checking analysis can be quite general. Chapter 10 will explain how, under appropriate finite reachability assumptions, we can model check any linear time temporal logic (LTL) property of a system specified in Maude as a system module. This chapter focuses on a simpler, yet very useful, model-checking capability, namely, the model checking of invariants, which can be accomplished just by using the search command.
Invariants are the most common and useful safety properties, that is, properties stating that something bad should never happen. Given a transition system and an initial state s0, an invariant I is a predicate defining a subset of states meeting two properties:
Therefore, an invariant is a predicate defining a set of states that contains all the states reachable from s0. If an invariant holds, that is, if it is truly an invariant satisfying the two properties above, then we know that something “bad” can never happen, namely, the negation ¬I of the invariant is impossible. In other words, we view ¬I as a bad property that should never happen, and I as a good property we want to ensure.
Given a rewrite theory = (Σ,E,ϕ,R) specified in Maude as a system module, we can define an
invariant I, yielding a decidable set of states, by:
The transition system implicit in this setting is one in which a one-step transition between two states, that is, between two elements [t],[t′] ∈ TΣ∕E,k, exists if and only if there is a representative t0 ∈ [t] and a one-step rewrite with the rules R, t0-→1t0′, such that t0′∈ [t′]. We introduce the notation
to state that the transition system associated with with state kind k and initial state init satisfies
the invariant I.
The key question now is: how can we automatically verify that an invariant I holds? The
answer is very simple. Assuming that = (Σ,E,ϕ,R) satisfies reasonable executability
conditions, namely, that E and R are finite sets, (Σ,E) is ground Church-Rosser and
terminating,1
and the rules R are ground coherent with E, and assuming, further, that all the conditions for rules in
R are purely equational, then I holds if and only if the search command
has no solutions. Indeed, having no solutions exactly means that on init, and on all states reachable from it, the predicate I evaluates to true, that is, that I is an invariant. Assuming that I has been fully defined in all cases (which is always easy with the owise feature, described in Section 4.5.4), so that it always evaluates to either true or false, we could instead give the command
Consider, for example, a simple clock that marks the hours of the day. Such a clock can be specified with the system module
A natural initial state is the state clock(0). Note that, in principle, the clock could be in an infinite number of states, such as clock(7633157) or clock(-33457129). The point, however, is that if our initial state is clock(0), then only states clock(T) with times T such that 0 <= T < 24 can be reached. This suggests making the predicate 0 <= T < 24 an invariant of our clock system.
Using simple linear arithmetic reasoning, we can express the negation of such an invariant as the predicate (T < 0) or (T >= 24); thus, we can automatically verify that our simple clock satisfies the invariant by giving the command:
If, as it is the case in this clock example, the number of states reachable from the initial state is finite, then search commands of this kind provide a decision procedure for the satisfaction of invariants. That is, in finite time Maude will either find no solutions to a search for a state violating the invariant, or will find a state violating the invariant together with a sequence of rewrites from the initial state to it, that is, a counterexample.
But what if the number of states reachable from the initial state is infinite? In such a case, if the invariant I is violated, the search command will terminate in finite time yielding a counterexample. Termination is guaranteed by the breadth-first nature of the search. The point is that such a counterexample is a reachable state; therefore, there is a finite sequence of rewrites from the initial state to such a violating state. Since there is only a finite number of rules R, and therefore a finite number of ways that each state can be rewritten, even though the number of reachable states is infinite, the number of states reachable from the initial state by a sequence of rewrites of length less than a given bound is always finite. This bounded subset is always explored in finite time by the search command. This means that, for systems where the set of reachable states is infinite, search becomes a semi-decision procedure for detecting the violation of an invariant. That is, if the invariant is violated, we are guaranteed to get a counterexample; but, if it is not violated, we will search forever, never finding it.
We can illustrate the semi-decision procedure nature of search for the verification of invariant failures with a simple infinite-state example of processes and resources. This example has some similarities with the classical dining philosophers problem, but it is on the one hand simpler (processes and resources have no identities or topology), and on the other hand more complex, since the number of processes and resources can grow dynamically in an unbounded manner.
The state is a soup (multiset) of processes and resources. Each process needs to acquire two resources. Originally, each process p contains the null state; but if a resource res is available, it can acquire it (rule acq1). If a second resource becomes available, it can also acquire it (rule acq2). After acquiring both resources and using them, the process can release them (rule rel). Furthermore, the number of processes and resources can grow in an unbounded manner by the duplication of each process-resource pair (rule dupl).
One invariant we might like to verify about this system is deadlock freedom. There are two ways to model check this property: one completely straightforward, and another requiring some extra work. The straightforward manner is to give the search command
Maude will indeed continue printing all the solutions it finds. But since there is an infinite number of deadlock states, it may be preferable to specify in advance a bound on the number of solutions, giving, for example, a command like the following, that looks for at most 5 solutions.
The nice thing about model checking deadlock freedom this way is that there is no need to explicitly specify the invariant as a Boolean predicate. This is because the negation of the invariant is by definition the set of deadlock states, which is what the search command with the =>! qualification precisely looks for.
If one wishes, one can, with a little more work, perform an equivalent model checking of the same property by using an explicit enabledness predicate. Of course, this cannot be done in the original module, because such a predicate has not been defined, but this is easy enough to do:
One can then give the command
getting the following 5 solutions:
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.
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:
We could try model checking these two invariants in two different ways:
To model check our two invariants using an implicit representation we could use the commands
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 105, with the commands:
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.
Then, we obtain a much better performance:
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.
The bounded model checking of our two invariants for the readers and writers example up to depth 106 greatly increases our confidence that the invariants hold, but, as already mentioned, bounded model checking is an incomplete procedure that falls short of being a proof: a counterexample at greater depth could exist.
Can we actually fully verify such invariants in an automatic way? One possible method is to verify
the invariants through search not on the original infinite-state system, but on a finite-state
abstraction of it, that is, on an appropriate quotient of the original system whose set of
reachable states is finite. The paper [88] describes a simple method for, given a rewrite
theory = (Σ,E,ϕ,R), defining an abstraction 
of it: just add equations. That is, we
can define our abstract theory as a rewrite theory = (Σ,E ∪ G,ϕ,R), with G a set
of extra equations powerful enough to collapse the infinite set of reachable states into a
finite set. This method can be used (with an additional deadlock-freedom requirement)
to verify not just invariants, but in fact any LTL formula (see [88] and Section 13.4 of
[21]).
Of course, the equations G we add cannot be arbitrary. First of all, they should respect all the necessary
executability assumptions, so that in = (Σ,E ∪G,ϕ,R) the equations E ∪G should be ground Church-Rosser
and terminating,2
and the rules R should be ground coherent with E ∪ G. Furthermore, the equations G should be
invariant-preserving with respect to the invariants that we want to model check; that is, for any such
invariant I and for any two ground terms t,t′ denoting states such that t = E∪Gt′, it should be the
case that E ⊢ I(t) = I(t′).
A first key observation is that, if both and protect the sort Bool, that is, the only
canonical forms of that sort are true and false, and true≠false, then the equations G are
invariant-preserving. A second key observation is that we may be able to automatically check that a
module protects the sort Bool by:
Indeed, since true and false are the only constructors of sort Bool, (4) ensures the “no junk” part of protection, whereas (1)–(3) ensure the “no confusion,” true≠false part.
For invariant verification, the key property that an abstraction meeting these requirements satisfies is that, if I is one of the invariants preserved by G, then we have the implication
Therefore, if we can verify the invariant on , we are sure that it also holds on . However, the fact
that we find a counterexample in does not necessarily mean that a counterexample exists for : it
could be a spurious counterexample, caused by being too coarse of an abstraction, and therefore
having no counterpart in . In such cases, one possible approach is to refine our abstraction by
imposing fewer equations.
We can illustrate these ideas by defining an abstraction of our readers-writers system. In order to check that the equations in our abstraction preserve the invariants, we need an explicit representation of those invariants. Since at present the CRC and MTT tools do not handle predefined modules like BOOL, we use instead a sort NewBool.
We can now define our abstraction, in which all the states having more than one reader and no writers are identified with the state having exactly one reader and no writer.
where the second including importation is needed because the READERS-WRITERS module is not protected, but would be assumed protected by default (because it is protected in READERS-WRITERS-PREDS) unless we explicitly declare it in including mode (see Section 6.1.3).
In order to check both the executability and the invariant-preservation properties of this abstraction, since we have no equations with either tt or ff in their lefthand side, we now just need to check:
Regarding termination, since the equations of READERS-WRITERS-ABS contain those of the module READERS-WRITERS-PREDS, it is enough to check the termination of the equations in the former. The MTT tool, using the AProVE termination tool, checks this automatically.
Once the READERS-WRITERS-ABS and READERS-WRITERS-PREDS modules are available in Full Maude (see Section 15.1), we can check confluence of the equations by invoking the CRC as follows:
which finishes task (1).
Regarding (2), the SCC tool gives us:
This leaves us with task (3), where the Coherence Checker (ChC) tool responds as follows:
Of course, ground coherence means that all ground instances of this pair can be rewritten by a one-step rewrite up to canonical form by the equations. We can reason by cases and decompose this critical pair into two:
Using the reduce command we can check that the canonical form of the term < s(s(N:Nat)), 0 > is < s(0), 0 >. Therefore, all we need to do is to check that < s(0), 0 > rewrites to itself (up to canonical form) in one step. We can do this check by giving the command:
We have therefore completed all the checks (1)–(3) and can now automatically verify the two invariants on the abstract system, and therefore conclude that they hold in our original infinite-state readers-writers system, by executing the search commands: