Publications

Efficient Symbolic Model Checking for Process Algebras

Authors
Josť Vander Meulen, Charles Pecheur
Tags
, , , , ,

Reduction, CTL

Title
Efficient Symbolic Model Checking for Process Algebras
Authors
Josť Vander Meulen, Charles Pecheur
 FWD_ImProviso.pdf Δ   202Kb   27 Apr 2010
Type
In Proceedings
Book title
Proceedings of 13th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2008), L'Aquila, Italy
Series
LNCS
Volume
5596
Publisher
Springer
Year
2008

Abstract

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 paper presents a new algorithm and a new tool 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. 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 of a large industrial model which cannot be handled by conventional model checkers.

Tags Tags: , , , , ,


BibTeX Record
  @INPROCEEDINGS{lvl-2008-1,
    TITLE = {Efficient Symbolic Model Checking for Process Algebras},
    AUTHOR = {Josť {Vander Meulen} and Charles Pecheur},
    YEAR = {2008},
    VOLUME = {5596},
    PUBLISHER = {Springer},
    SERIES = {LNCS},
    URL = {http://lvl.info.ucl.ac.be/Publications/EfficientSymbolicModelCheckingForProcessAlgebras},
  }