Model Checking Procedures for Infinite State Systems

9 years 10 months ago
Model Checking Procedures for Infinite State Systems
The paper depicts experiments and results with preditraction based verification applied to infinite state Predicate abstraction is a method for automatic tion of abstract state space that can be used by any common finite state model checking tool, such as NuSMV. used abstract state space and NuSMV tool to verify safety properties of infinite state mutual exclusion protocols. ugh 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.
Nikola Bogunovi, Edgar Pek
Added 22 Aug 2010
Updated 22 Aug 2010
Type Conference
Year 2006
Where ECBS
Authors Nikola Bogunovi, Edgar Pek
Comments (0)