## SummaryThe Maude Invariant Analyzer Tool is a tool designed for proving two key safety properties of executable Maude specifications, namely, ground stability and ground invariance, plus their combination by strengthening techniques. The tool mechanizes an inference system that, without assuming finiteness of the set of initial or reachable states, uses rewriting and narrowing-based reasoning techniques, in which all temporal logic formulas eventually disappear and are replaced by purely equational conditional sentences. The Maude Invariant Analyzer Tool provides a substantial degree of mechanization and can automatically discharge many proof obligations without user intervention.
## InstallationThe Maude Invariant Analyzer Tool (InvA) is entirely written in Maude. The current version works on Maude 2.6-alpha and requires Full Maude 2.6, and the Church-Rosser Checker 3.
- Download InvA 0.2a (includes Full Maude 2.6 and the Church-Rosser Checker 3).
- Download Maude 2.6 alpha
The analyzer source is in file
`inva.maude` .## UsageYou must first make sure the invariant analyzer is loaded. Assuming the analyzer source
`inva.maude` is in the current directory and `maude` is your Maude executable, you can load it using the command:`[inva] maude inva.maude ` ` \||||||||||||||||||/` ` --- Welcome to Maude ---` ` /||||||||||||||||||\` ` Maude 2.6 built: Dec 10 2010 11:12:39` ` Copyright 1997-2010 SRI International` ` Wed May 18 15:40:27 2011` ` Full Maude 2.6e July 7th 2012` ` Invariant Analyzer 0.2a - April 17th 2012` ` (with Church-Rosser Checker 3m)` The Maude Invariant Analyzer Tool provides several commands, which can be listed by using the
`(help .)` command:`(` `analyze-stable` ` <pred> ` `in` ` <fmodule> <module> ` `.` `)` `generates the proof obligations for the ground` `<pred> -stability of the topmost rewrite theory` `specified by <module> under the equational definition` `of <pred> in the equational theory specified by <fmodule>;` `it tries to discharge the proof obligations and shows the` `simplified version of the ones that could not be dischared` `(` `analyze-stable` ` <pred> ` `in` ` <fmodule> <module> ` `using` ` <pred> ` `.` `)` `the same as above but assuming the top most rewrite theory` `is ground invariant for the second <pred>` `(` `analyze` ` <pred> ` `implies` ` <pred> ` `in` ` <fmodule> ` `.` `)` `generates the proof obligations for the given implication` `to hold under the equational definitions in <fmodule>;` `it tries to discharge the proof obligations and shows the` `simplified version of the ones that could not be discharged` `(` `show pos` ` .)` `shows the simplified proof obligations that could not be` `discharged by the last analyze or analyze-stable command` `(` `show-all pos .` `)` `shows the proof obligations generated by the last analyze` `or analyze-stable command` `(` `help .` `)` `shows this help menu` You enter in modules that you are interested in checking using the usual Maude syntax. The analyzer makes a distinction between
the
system module under verification and the functional module specifying the state predicates.Consider the following specification of a readers-writers system:
`fmod R&W-SYNTAX is` ` sort Nat .` ` op 0 : -> Nat [ctor] .` ` op s : Nat -> Nat [ctor] . ` ` sort State .` ` op <_,_> : Nat Nat -> State [ctor] .` `endfm` `mod R&W is` ` pr R&W-SYNTAX .` ` vars R W : Nat .` ` rl [w-enter] : < 0, 0 > => < 0, s(0) > .` ` rl [w-leave] : < R, s(W) > => < R, W > .` ` rl [r-enter] : < R, 0 > => < s(R), 0 > .` ` rl [r-leave] : < s(R), W > => < R, W > .` `endm` Functional module R&W-SYNTAX defines the syntax of the readers-writers system and module R&W its four concurrent transitions. A state is represented by a pair
`<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 any state without writers, we want to prove that
`R&W` achieves mutual exclusion, namely, readers and writers never access the resource simultaneously. Observe that the set of initial states is infinite and also that the number of processes is unbounded. We specify two state predicates, one for the initial states and one for the mutual exclusion property, in functional module `R&W-PROPS` . `fmod R&W-PROPS is` ` pr R&W-SYNTAX .` ` vars R W : Nat .` ` ops init mutex : State -> [Bool] .` ` --- set of initial states` ` eq [init] : init(< R, 0 >) = true .` ` --- mutual exclusion between readers and writers` ` eq [w=0] : mutex(< R, 0 >) = true .` ` eq [r=0] : mutex(< 0, W >) = true .` ` eq [no-mutex] : mutex(< s(R), s(W) >) = false .` `enfm` Assuming file
`inva.maude` has been loaded, and file `r+w.maude` contains modules R&W-SYNTAX, R&W, and R&W-PROPS, the following is a transcript of an interactive proof of the property we are interested:`Maude> load r+w.maude ` `Maude> select INVA .` `Maude> loop init .` `Maude> (analyze init(S:State) implies mutex(S:State) in R&W-PROPS .)` `rewrites: 3349 in 15ms cpu (19ms real) (214390 rewrites/second)` `Checking R&W-PROPS ||- init => mutex ...` `Proof obligations generated: 1` `Proof obligations discharged: 1` `Success!` `Maude> (analyze-stable mutex(S:State) in R&W-PROPS R&W .)` `rewrites: 9695 in 15ms cpu (17ms real) (621753 rewrites/second)` `Checking R&W ||- mutex => O mutex ...` `Proof obligations generated: 8` `Proof obligations discharged: 8` `Success!` ## PublicationsThe Maude Invariant Analyzer Tool is described in the CALCO11 paper. The technical report is an extension of the paper with proofs and a more detailed example. |

software >