Partial Model Checking using Networks of Labelled Transition Systems and Boolean Equation Systems

Frederic Lang 1, * Radu Mateescu 1
* Auteur correspondant
1 CONVECS - Construction of verified concurrent systems
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
Abstract : Partial model checking was proposed by Andersen in 1995 to verify a temporal logic formula compositionally on a composition of processes. It consists in incrementally incorporating into the formula the behavioural information taken from one process - an operation called quotienting - to obtain a new formula that can be verified on a smaller composition from which the incorporated process has been removed. Simplifications of the formula must be applied at each step, so as to maintain the formula at a tractable size. In this paper, we revisit partial model checking. First, we extend quotienting to the network of labelled transition systems model, which subsumes most parallel composition operators, including $m$-among-$n$ synchronisation and parallel composition using synchronisation interfaces, available in the ELOTOS standard. Second, we reformulate quotienting in terms of a simple synchronous product between a graph representation of the formula (called formula graph) and a process, thus enabling quotienting to be implemented efficiently and easily, by reusing existing tools dedicated to graph compositions. Third, we propose simplifications of the formula as a combination of bisimulations and reductions using Boolean equation systems applied directly to the formula graph, thus enabling formula simplifications also to be implemented efficiently. Finally, we describe an implementation in the CADP (Construction and Analysis of Distributed Processes) toolbox and present some experimental results in which partial model checking uses hundreds of times less memory than on-the-fly model checking.
Type de document :
Article dans une revue
Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2013, 9 (4), 〈http://www.lmcs-online.org/ojs/viewarticle.php?id=1241&layout=abstract〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-00872181
Contributeur : Frederic Lang <>
Soumis le : vendredi 11 octobre 2013 - 13:40:23
Dernière modification le : mercredi 11 avril 2018 - 01:53:21
Document(s) archivé(s) le : dimanche 12 janvier 2014 - 04:34:08

Fichier

Lang-Mateescu-13-final.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00872181, version 1

Citation

Frederic Lang, Radu Mateescu. Partial Model Checking using Networks of Labelled Transition Systems and Boolean Equation Systems. Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2013, 9 (4), 〈http://www.lmcs-online.org/ojs/viewarticle.php?id=1241&layout=abstract〉. 〈hal-00872181〉

Partager

Métriques

Consultations de la notice

429

Téléchargements de fichiers

137