TY - GEN
T1 - Convergence verification
T2 - 6th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2008
AU - Chandy, K. Mani
AU - Mitra, Sayan
AU - Pilotto, Concetta
N1 - Funding Information:
The work is funded in part by the Caltech Information Science and Technology Center and AFOSR MURI FA9550-06-1-0303.
PY - 2008
Y1 - 2008
N2 - 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 the class of systems in which an agent's state 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.
AB - 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 the class of systems in which an agent's state 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.
UR - http://www.scopus.com/inward/record.url?scp=53049094638&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=53049094638&partnerID=8YFLogxK
U2 - 10.1007/978-3-540-85778-5_16
DO - 10.1007/978-3-540-85778-5_16
M3 - Conference contribution
AN - SCOPUS:53049094638
SN - 354085777X
SN - 9783540857778
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 218
EP - 232
BT - Formal Modeling and Analysis of Timed Systems - 6th International Conference, FORMATS 2008, Proceedings
Y2 - 15 September 2008 through 17 September 2008
ER -