Model Checking Procedures for Infinite State Systems (CROSBI ID 517045)
Prilog sa skupa u zborniku | izvorni znanstveni rad | međunarodna recenzija
Podaci o odgovornosti
Bogunović, Nikola ; Pek, Edgar
engleski
Model Checking Procedures for Infinite State Systems
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.
predicate abstraction; model checking; mutual exclusion protocols; infinite state systems
nije evidentirano
nije evidentirano
nije evidentirano
nije evidentirano
nije evidentirano
nije evidentirano
Podaci o prilogu
419-425-x.
2006.
objavljeno
Podaci o matičnoj publikaciji
Riebisch, Matthias ; Tabeling, Peter ; Zorn, Werner
Los Alamitos (CA): IEEE Computer Society Conference Publishing Service
Podaci o skupu
13th Annual IEEE Engineering Symposium and Workshop on Engineering of Computer-Based Systems: Mastering the Complexity of Computer-Based Systems
predavanje
27.03.2006-30.03.2006
Potsdam, Njemačka