Mateescu-Thivolle-08

**A Model Checking Language for Concurrent Value-Passing Systems**

*Radu Mateescu and Damien Thivolle*

Proceedings of the 15th International Symposium on Formal Methods FM'08 (Turku, Finland), May 2008

** Abstract:**

Modal mu-calculus is an expressive specification formalism for
temporal properties of concurrent programs represented as Labeled
Transition Systems (LTSs). However, its practical use is hampered by
the complexity of the formulas, which makes the specification task
difficult and error-prone. In this paper, we propose MCL (*Model
Checking Language*), an enhancement of modal mu-calculus with
high-level operators aimed at improving expressiveness and conciseness
of formulas. The main MCL ingredients are parameterized fixed points,
action patterns extracting data values from LTS actions, modalities on
transition sequences described using extended regular expressions and
programming language constructs, and an infinite looping operator
specifying fairness. We also present a method for on-the-fly model
checking of MCL formulas on finite LTSs, based on the local resolution
of boolean equation systems, which has a linear-time complexity for
alternation-free and fairness formulas. MCL is supported by the
EVALUATOR 4.0 model checker developed within the CADP verification
toolbox.

16 pages | PostScript |

Cumulated slides about EVALUATOR 4.0 by R. Mateescu and D. Thivolle |