Formal Verification of Concurrent Systems via Directed Model Checking

Sara Gradara 1 Antonella Santone 1 Maria Luisa Villani 1
1 RCOST
Abstract : Model checking suffers from the state explosion problem, due to the exponential increase in the size of a finite state model as the number of system components grows. Directed model checking aims at reducing this problem through heuristic-based search strategies. The model of the system is built while checking the formula and this construction is guided by some heuristic function. In this line, we have defined a structure-based heuristic function operating on processes described in the Calculus of Communicating Systems (CCS), which accounts for the structure of the formula to be verified, expressed in the selective Hennessy-Milner logic. We have implemented a tool to evaluate the method and verified a sample of well known CCS processes with respect to some formulae, the results of which are reported and commented.
Keywords : model checking heuristic search CCS logic
Type de document :
Communication dans un congrès
Stephan Merz et Tobias Nipkow. Automatic Verification of Critical Systems, Sep 2006, Nancy, France, pp.132-144, 2006, Automatic Verification of Critical Systems (AVoCS 2006)
Liste complète des métadonnées
https://hal.inria.fr/inria-00089489
Contributeur : Stephan Merz <>
Soumis le : vendredi 18 août 2006 - 19:06:09
Dernière modification le : vendredi 18 août 2006 - 19:58:02
Document(s) archivé(s) le : mardi 6 avril 2010 - 00:37:52

Fichier

SANTONE.pdf

Identifiants

  • HAL Id : inria-00089489, version 1

Collections

AVOCS06

Citation

Sara Gradara, Antonella Santone, Maria Luisa Villani. Formal Verification of Concurrent Systems via Directed Model Checking. Stephan Merz et Tobias Nipkow. Automatic Verification of Critical Systems, Sep 2006, Nancy, France, pp.132-144, 2006, Automatic Verification of Critical Systems (AVoCS 2006). 〈inria-00089489〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

114

Téléchargements de fichiers

126

Contact


archive-ouverte@inria.fr