2008 | OriginalPaper | Chapter
A Model Checking Language for Concurrent Value-Passing Systems
Authors : Radu Mateescu, Damien Thivolle
Published in: FM 2008: Formal Methods
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
Modal
μ
-calculus is an expressive specification formalism for temporal properties of concurrent programs represented as Labeled Transition Systems (
Lts
s). 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
μ
-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
Lts
s, 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.