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 <>
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