A Model Checking Language for Concurrent Value-Passing Systems

Radu Mateescu 1 Damien Thivolle 1
1 VASY - System validation - Research and applications
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
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.
Type de document :
Communication dans un congrès
Jorge Cuellar and Tom Maibaum. FM 2008, May 2008, Turku, Finland. Springer Verlag, 5014, pp.148-164, 2008, Lecture Notes in Computer Science. 〈10.1007/978-3-540-68237-0_12〉
Liste complète des métadonnées

Littérature citée [40 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00315312
Contributeur : Radu Mateescu <>
Soumis le : jeudi 28 août 2008 - 10:14:04
Dernière modification le : mercredi 11 avril 2018 - 01:54:43
Document(s) archivé(s) le : jeudi 3 juin 2010 - 19:04:06

Fichier

Mateescu-Thivolle-08.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Radu Mateescu, Damien Thivolle. A Model Checking Language for Concurrent Value-Passing Systems. Jorge Cuellar and Tom Maibaum. FM 2008, May 2008, Turku, Finland. Springer Verlag, 5014, pp.148-164, 2008, Lecture Notes in Computer Science. 〈10.1007/978-3-540-68237-0_12〉. 〈inria-00315312〉

Partager

Métriques

Consultations de la notice

300

Téléchargements de fichiers

170