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