Symbolic Model Checking of Asynchronous Systems
Model checking is an efficient technique for verifying properties on reactive systems. BDD-based symbolic model checking is a well-known approach to deal with the state space explosion problem in model checking, though BDDs can still suffer from space blow-up. More recently, bounded model checking using SAT-based procedures has been used as a very successful alternative to BDDs. However, these approaches give poor results when it is applied to models with a lot of asynchronism. On the other hand, partial-order reduction (POR) methods reduce the number of states explored by model-checking, by avoiding to explore different equivalent interleavings of concurrent events. We are developing, implementing and experimenting with algorithms which combine partial-order reduction and symbolic model checking to allow more efficient verification on models featuring asynchronous processes.
LVL Members: José Vander Meulen, Charles Pecheur
External Partners: None
Related Publications:
- Combining Partial Order Reduction with Symbolic Model Checking. José Vander Meulen?. Doctoral thesis, Université catholique de Louvain.
- Combining Partial Order Reduction and Symbolic Model Checking to verify LTL properties. José Vander Meulen?, Charles Pecheur . NASA FORMAL METHODS 2011.
- Milestones: A Model Checker Combining Symbolic Model Checking and Partial Order Reduction. José Vander Meulen?, Charles Pecheur. NASA FORMAL METHODS 2011.
- Combining Partial Order Reduction with Bounded Model Checking. José Vander Meulen?, Charles Pecheur. Proceedings of Communicating Process Architectures 2009, Eindhoven, Netherlands.
- Efficient Symbolic Model Checking for Process Algebras. José Vander Meulen?, Charles Pecheur. Proceedings of 13th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2008), L'Aquila, Italy.
Tags: -
Find It
Sections
Verification Diagnosis Autonomy ModelChecking Planning PDDL Requirements Testing LTL ThemeCoverage HumanComputerInteraction UserModel ProjectMOVES ThemeHMI LVL Website SymbolicModelChecking CTL Actions SMV EpistemicLogic ProjectNASA PartialOrderReduction BoundedModelChecking ThemePOR TemporalLogic Simulation Tools Tutorial Publication Equivalences