Naslov
Verification of Infinite State Mutual Exclusion Protocols

Autori
Pek, Edgar ; Bogunović, Nikola

Vrsta, podvrsta i kategorija rada
Radovi u zbornicima skupova, cjeloviti rad (in extenso), znanstveni

Izvornik
Proceedings of the Joint Conferences Computers in Technical systems and Intelligent systems / Budin, Leo ; Ribarić Slobodan - Rijeka : Hrvatska udruga za informacijsku i komunikacijsku tehnologiju, elektroniku i mikroelektroniku - MIPRO, 2005, 19-24

Skup
Computers in Technical Systems

Mjesto i datum
Opatija, Hrvatska, 30.05.2005. - 03.06.2005

Vrsta sudjelovanja
Predavanje

Vrsta recenzije
Međunarodna recenzija

Ključne riječi
formal verification; predicate abstraction; mutual exclusion

Sažetak
In this work we present formal verification of two infinite state mutual exclusion protocols. Infinite state systems cannot be verified by automatic algorithmic verification techniques such as model checking. On the other hand, deductive verification can be used in infinite state verification, but it is time consuming and requires considerable expertise. We combine algorithmic and deductive verification using the abstract interpretation framework. A methodology from that framework called predicate abstraction allows us to reduce infinite state systems to finite state using decision procedures. The obtained finite state system can be model checked against restricted class of temporal logic formulas. That restricted class is expressive enough for specification of the safety properties, and can be verified with NuSMV tool.

Izvorni jezik
Engleski

Znanstvena područja
Računarstvo

POVEZANOST RADA