engleski

Verification of Infinite State Mutual Exclusion Protocols

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.

formal verification; predicate abstraction; mutual exclusion

nije evidentirano