State space abstraction for parameterized self-stabilizing embedded systems

Nikolaos Liveris*, Hai Zhou, Robert P. Dick, Prithviraj Banerjee

*Corresponding author for this work

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

Abstract

Self-stabilizing systems are systems that automatically recover from any transient fault. Proving the correctness of a parameterized self-stabilizing system, i.e., a system composed of an arbitrary number of processes, is a challenging task. For the verification of parameterized systems the method of control abstraction has been developed. However, control abstraction can only be applied to systems in which each process has a fixed number of observable variables. In this article, we propose a technique to abstract a parameterized self-stabilizing system, whose processes have a parameterized number of observable variables, to a system with fixed number of observable variables. This enables the use of control abstraction for verification. The proposed technique targets low-atomicity, shared-memory, asynchronous systems. We establish the completeness of the method under reasonable conditions and demonstrate its effectiveness by applying it on a number of self-stabilizing distributed systems.

Original languageEnglish (US)
Title of host publicationProceedings of the 8th ACM International Conference on Embedded Software, EMSOFT'08
PublisherAssociation for Computing Machinery (ACM)
Pages11-20
Number of pages10
ISBN (Print)9781605584683
StatePublished - Jan 1 2008
Event8th ACM International Conference on Embedded Software, EMSOFT 2008 - Atlanta, GA, United States
Duration: Oct 19 2008Oct 24 2008

Publication series

NameProceedings of the 8th ACM International Conference on Embedded Software, EMSOFT'08

Other

Other8th ACM International Conference on Embedded Software, EMSOFT 2008
Country/TerritoryUnited States
CityAtlanta, GA
Period10/19/0810/24/08

Keywords

  • Abstraction
  • Network invariants
  • Parameterized systems
  • Self-stabilizing systems
  • Verification

ASJC Scopus subject areas

  • Software

Fingerprint

Dive into the research topics of 'State space abstraction for parameterized self-stabilizing embedded systems'. Together they form a unique fingerprint.

Cite this