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
FM2018 Δ   0Kb   28 May 2020
Fmics2013 Δ   0Kb   28 May 2020
GandALF2017 Δ   0Kb   28 May 2020
HMI2011 Δ   0Kb   28 May 2020
LVLPrivate Δ   0Kb   28 May 2020
LVLPrivateNews Δ   0Kb   28 May 2020
Main Δ   0Kb   28 May 2020
Members Δ   0Kb   28 May 2020
Publications Δ   4Kb   28 May 2020
Site Δ   0Kb   28 May 2020
Talks Δ   4Kb   28 May 2020
Tools Δ   0Kb   28 May 2020
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 = {https://lvl.info.ucl.ac.be/Publications/EfficientSymbolicModelCheckingForProcessAlgebras},
  }