Efficient Symbolic Model Checking for Process Algebras

José Vander Meulen
Friday, 3 April, 2009 (All day)

Different approaches have been developed to mitigate the state space explosion of model checking techniques. Among them, symbolic verification techniques use efficient representations such as BDDs to reason over sets of states rather than over individual states. Unfortunately, past experience has shown that these techniques do not work well for loosely-synchronized models. This talk presents a new algorithm that combines BDD-based model checking with partial order reduction (POR) to allow the verification of models featuring asynchronous processes, with significant performance improvements over currently available tools. We start from the ImProviso algorithm (Lerda et al.) for computing reachable states, which combines POR and symbolic verification. We merge it with the FwdUntil method (Iwashita et al.) that supports verification of a subset of CTL. Then, we present how is possible to extend this algorithm, in order to apply it with Bounded Model Checking methods for checking LTL properties. Our algorithm has been implemented in a prototype that is applicable to action-based models and logics such as process algebras and ACTL. Experimental results on a model of an industrial application show that our method can verify properties for sizes which cannot be handled by conventional model checkers.