Handling Parameterized Systems with Non-atomic Global Conditions

Parosh Aziz Abdulla, Noomene Ben Henda, Giorgio Delzanno, Ahmed Rezine

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 while 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.

In Proceedings of the 9th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), 2008,

Last version (pdf) 2008