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

https://hal.inria.fr/inria-00089489
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

Identifiers

  • HAL Id : inria-00089489, version 1

Collections

Citation

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⟩

Share

Metrics

Record views

179

Files downloads

368