Model checking procedures for infinite state systems
2006pp. 7 pp.–425
Citations Over Time
Abstract
The paper depicts experiments and results with predicate abstraction based verification applied to infinite state systems. Predicate abstraction is a method for automatic construction of abstract state space that can be used by any common finite state model checking tool, such as NuSMV. We have used abstract state space and NuSMV tool to verify safety properties of infinite state mutual exclusion protocols. Even though predicate abstraction allows model checking against a restricted class of temporal logic formulas, we have shown that the restricted class is expressive enough to specify basic safety properties. Our experiments were conducted on Bakery and Fischer mutual exclusion protocols.
Related Papers
- → Model Checking Software via Abstraction of Loop Transitions(2003)7 cited
- → Model checking procedures for infinite state systems(2006)2 cited
- → Automated Predicate Abstraction for Real-Time Models(2009)3 cited
- On computing invariants for predicate abstraction by SAT-solving(2009)
- → Abstraction Continued(1998)