Pregled bibliografske jedinice broj: 246961
Model Checking Procedures for Infinite State Systems
Model Checking Procedures for Infinite State Systems // Proceedings of the 13th IEEE International Symposium and Workshop on Engineering of Computer-Based Systems: Mastering the Complexity of Computer-Based Systems / Riebisch, Matthias ; Tabeling, Peter ; Zorn, Werner (ur.).
Los Alamitos (CA): IEEE Computer Society Conference Publishing Service, 2006. str. 419-425 (predavanje, međunarodna recenzija, cjeloviti rad (in extenso), znanstveni)
CROSBI ID: 246961 Za ispravke kontaktirajte CROSBI podršku putem web obrasca
Naslov
Model Checking Procedures for Infinite State Systems
Autori
Bogunović, Nikola ; Pek, Edgar
Vrsta, podvrsta i kategorija rada
Radovi u zbornicima skupova, cjeloviti rad (in extenso), znanstveni
Izvornik
Proceedings of the 13th IEEE International Symposium and Workshop on Engineering of Computer-Based Systems: Mastering the Complexity of Computer-Based Systems
/ Riebisch, Matthias ; Tabeling, Peter ; Zorn, Werner - Los Alamitos (CA) : IEEE Computer Society Conference Publishing Service, 2006, 419-425
Skup
13th Annual IEEE Engineering Symposium and Workshop on Engineering of Computer-Based Systems: Mastering the Complexity of Computer-Based Systems
Mjesto i datum
Potsdam, Njemačka, 27.03.2006. - 30.03.2006
Vrsta sudjelovanja
Predavanje
Vrsta recenzije
Međunarodna recenzija
Ključne riječi
predicate abstraction; model checking; mutual exclusion protocols; infinite state systems
Sažetak
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.
Izvorni jezik
Engleski
Znanstvena područja
Računarstvo
