Formal Verification of Concurrent Systems via Directed Model Checking - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2006

Formal Verification of Concurrent Systems via Directed Model Checking

Sara Gradara
  • Fonction : Auteur
  • PersonId : 834673
Antonella Santone
  • Fonction : Auteur
  • PersonId : 834674
Maria Luisa Villani
  • Fonction : Auteur
  • PersonId : 834675

Résumé

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.
Fichier principal
Vignette du fichier
SANTONE.pdf (217.52 Ko) Télécharger le fichier

Dates et versions

inria-00089489 , version 1 (18-08-2006)

Identifiants

  • HAL Id : inria-00089489 , version 1

Citer

Sara Gradara, Antonella Santone, Maria Luisa Villani. Formal Verification of Concurrent Systems via Directed Model Checking. Automatic Verification of Critical Systems, Sep 2006, Nancy, France, pp.132-144. ⟨inria-00089489⟩

Collections

AVOCS06
50 Consultations
146 Téléchargements

Partager

Gmail Facebook X LinkedIn More