| HAL-Inria | Publications, software ... of Inria's scientists |
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.
https://hal.inria.fr/inria-00089489
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
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