HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Conference papers

Formal Verification of Concurrent Systems via Directed Model Checking

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.
Document type :
Conference papers
Complete list of metadata

Contributor : Stephan Merz Connect in order to contact the contributor
Submitted on : Friday, August 18, 2006 - 7:06:09 PM
Last modification on : Friday, August 18, 2006 - 7:58:02 PM
Long-term archiving on: : Tuesday, April 6, 2010 - 12:37:52 AM


  • HAL Id : inria-00089489, version 1



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⟩



Record views


Files downloads