Convergence verification: From shared memory to partially synchronous systems

K. Mani Chandy, Sayan Mitra, Concetta Pilotto

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.

Original languageEnglish (US)
Title of host publicationFormal Modeling and Analysis of Timed Systems - 6th International Conference, FORMATS 2008, Proceedings
Pages218-232
Number of pages15
DOIs
StatePublished - 2008
Externally publishedYes
Event6th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2008 - Saint Malo, France
Duration: Sep 15 2008Sep 17 2008

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume5215 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other6th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2008
CountryFrance
CitySaint Malo
Period9/15/089/17/08

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Convergence verification: From shared memory to partially synchronous systems'. Together they form a unique fingerprint.

Cite this