Convergence Verification: From Shared Memory to Partially Synchronous Systems

Proceedings of the 6th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS`08) , LNCS 5215, 217-231, September 2008, Springer

Verification of partially synchronous distributed systems is difficult because of inherent concurrency and the potentially large state space of the channels. This paper identifies a subclass of such systems for which convergence properties can be verified based on the proof of convergence for the corresponding discrete-time shared state system. The proof technique extends to a class of partially synchronous systems in which an agent's state also evolves continuously over time. The proof technique has been formalized in the PVS interface for timed I/O automata and applied to verify convergence of a mobile agent pattern formation algorithm.

FORMATS08.pdf333.28 KB