The Maude Invariant Analyzer Tool

Summary

The 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.

Installation

The 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.

Usage

You 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!

Publications

The 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.