This paper presents an efficient procedure to perform model checking of a concurrent process against a temporal logic formula, through the checking of a simulation between the description of the system and of the formula in the same formalism. The approach is applied, as an example, to processes defined through a specification language very compact, the well-know Calculus of Communicating Systems (CCS) defined by Milner, but it can be applied also to different languages as Lotos and CSP. The algorithm to explore the search space for the simulation problem is based on a greedy technique. The experiments show that a considerable reduction of both state space size and time can be achieved with respect to traditional model checking algorithms.
Model checking safety properties through simulation and heuristic search
De Francesco, Nicoletta;Lettieri, Giuseppe;Santone, Antonella
;Vaglini, Gigliola
2013-01-01
Abstract
This paper presents an efficient procedure to perform model checking of a concurrent process against a temporal logic formula, through the checking of a simulation between the description of the system and of the formula in the same formalism. The approach is applied, as an example, to processes defined through a specification language very compact, the well-know Calculus of Communicating Systems (CCS) defined by Milner, but it can be applied also to different languages as Lotos and CSP. The algorithm to explore the search space for the simulation problem is based on a greedy technique. The experiments show that a considerable reduction of both state space size and time can be achieved with respect to traditional model checking algorithms.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
