Efficient Symbolic Model Checking for Process Algebras
- 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: Symbolic Model Checking, Process Algebra, Partial Order Reduction, CTL, Project MOVES, Theme POR
- 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}, }