Handling parameterized systems with non-atomic global conditions
2008 (English)In: Verification, Model Checking, and Abstract Interpretation / [ed] Logozzo F; Peled DA; Zuck LD, Berlin: Springer-Verlag , 2008, 22-36 p.Conference paper (Refereed)
We consider verification of safety properties for parameterized systems with linear topologies. A process in the system is an extended automaton, where the transitions are guarded by both local and global conditions. The global conditions are non-atomic, i.e., a process allows arbitrary interleavings with other transitions white checking the states of all (or some) of the other processes. We translate the problem into model checking of infinite transition systems where each configuration is a labeled finite graph. We derive an over-approximation of the induced transition system, which leads to a symbolic scheme for analyzing safety properties. We have implemented a prototype and run it on several nontrivial case studies, namely non-atomic versions of Burn's protocol, Dijkstra's protocol, the Bakery algorithm, Lamport's distributed mutual exclusion protocol, and a two-phase commit protocol used for handling transactions in distributed systems. As far as we know, these protocols have not previously been verified in a fully automated framework.
Place, publisher, year, edition, pages
Berlin: Springer-Verlag , 2008. 22-36 p.
, Lecture Notes in Computer Science, 4905
IdentifiersURN: urn:nbn:se:uu:diva-106056DOI: 10.1007/978-3-540-78163-9_7ISI: 000253940200007OAI: oai:DiVA.org:uu-106056DiVA: diva2:223654
9th International Conference on Verification, Model Checking, and Abstract Interpretation San Francisco, CA, JAN 07-09, 2008