What is CADP?
Home Page Tools Overview Current Status Recent Changes
Installation
How to obtain CADP? Usage Statistics
Documentation
FAQ Tutorials Publications Manual Pages Demo Examples Wikipedia
CADP Community
Newsletters Education & Training Case Studies Research Tools
CADP Resources
VLSAT Benchmarks VLTS Benchmarks Other Resources
About CADP
Contributors

Table of Contents

Name

evaluator - a family of on-the-fly model checkers

Description

evaluator denotes a family of on-the-fly model checkers of CADP based on the modal mu-calculus. These tools take as inputs a Labelled Transition System (LTS) and a temporal logic formula, and produce as output a verdict indicating whether the LTS satisfies the formula or not, optionally accompanied by a diagnostic (fragment of the LTS) illustrating the verdict.

On the theoretical side, these model checkers rely on the resolution of Boolean Equation Systems (BES), Parameterized Boolean Equation Systems (PBES), and Linear Equation Systems (LES). On the practical side, they are implemented using the OPEN/CAESAR framework of CADP for on-the-fly verification.

Three versions of evaluator are currently available:

• evaluator3 (see the evaluator3 manual page) is an on-the-fly model checker for MCL version 3, an extension of the alternation-free mu-calculus with action predicates and regular expressions over action sequences. In the temporal formulas of MCL version 3, LTS actions are merely character strings. See the mcl3 manual page for details.

• evaluator4 (see the evaluator4 manual page) is an on-the-fly model checker for MCL version 4, an extension of MCL version 3 with data-handling constructs (data variables, expressions, parameterized fixed point operators, programming language constructs) and an infinite looping operator able to express fairness properties. In the temporal formulas of MCL version 4, LTS actions are tuples containing channel names and data values, which can be extracted and used in calculations. See the mcl4 manual page for details.
• evaluator5 (see the evaluator5 manual page) is an on-the-fly model checker for MCL version 5, an extension of MCL version 4 with a probabilistic operator specifying the probability of transition sequences characterized by generalized regular formulas. This probabilistic operator is interpreted on Probabilistic Transition Systems (PTSs), which are LTSs whose actions contain channel names, data values, and probabilities. See the mcl5 manual page for details.

Note: Currently, for backward compatibility reasons, evaluator (located in $CADP/bin.*/evaluator.a) is a shorthand for evaluator3 (located in $CADP/bin.*/evaluator3.a).

History and Authors

Versions 1.x and 2.x of EVALUATOR were developed by Marius Dorel Bozga (IMAG) and used an on-the-fly BES resolution algorithm proposed by J-C. Fernandez and L. Mounier. These versions, which accepted as input alternation-free modal mu-calculus (without regular expressions), are no longer available.

Version 3.0 of EVALUATOR was developed by Radu Mateescu and Mihaela Sighireanu (both at INRIA/VASY) and used a completely new on-the-fly BES resolution algorithm. Hubert Garavel (INRIA/VASY) suggested the enhancement of action formulas with the string concatenation operator, which was implemented by David Champelovier (INRIA/VASY).

Versions 3.5 and 3.6 of EVALUATOR replaced the dedicated BES resolution algorithm by the more general algorithms available in the caesar_solve_1 library of OPEN/CAESAR for on-the-fly BES resolution. All of this was implemented by Radu Mateescu (INRIA/VASY).

Version 4.0 of EVALUATOR handles version 4 of the MCL language. It was implemented by Radu Mateescu and Damien Thivolle (both at INRIA/VASY).

Version 5.0 of EVALUATOR handles version 5 of the MCL language. It was implemented by Radu Mateescu (INRIA/CONVECS).

See Also

evaluator3 , evaluator4 , evaluator5 , mcl , mcl3 , mcl4 , mcl5

Additional information is available from the CADP Web page located at http://cadp.inria.fr

Directives for installation are given in files $CADP/INSTALLATION_*.

Recent changes and improvements to this software are reported and commented in file $CADP/HISTORY.

Bugs

Please report bugs to Radu.Mateescu@inria.fr

---

Table of Contents

• Name
• Description
• History and Authors
• See Also
• Bugs