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: