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.

• Type: Conference
• Year: 2006
• Where: ECBS
• Authors: Nikola Bogunovi, Edgar Pek
• Keywords: Abstract State Space, ECBS 2006, Hardware, Mutual Exclusion Protocols, Predicate Abstraction