Published August 29, 2008
| public
Book Section - Chapter
Convergence Verification: From Shared Memory to Partially Synchronous Systems
- Creators
- Chandy, K. Mani
- Mitra, Sayan
- Pilotto, Concetta
- Others:
- Cassez, Franck
- Jard, Claude
Abstract
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.
Additional Information
© 2008 Springer-Verlag Berlin Heidelberg. The work is funded in part by the Caltech Information Science and Technology Center and AFOSR MURI FA9550-06-1-0303.Additional details
- Eprint ID
- 101520
- Resolver ID
- CaltechAUTHORS:20200225-075817665
- Caltech Information Science and Technology Center
- Air Force Office of Scientific Research (AFOSR)
- FA9550-06-1-0303
- Created
-
2020-02-25Created from EPrint's datestamp field
- Updated
-
2021-11-16Created from EPrint's last_modified field
- Series Name
- Lecture Notes in Computer Science
- Series Volume or Issue Number
- 5215