An approach to preserve protocol consistency and executability across updates

Mahadevan Subramaniam, Parvathi Chundi

Research output: Chapter in Book/Report/Conference proceedingChapter

Abstract

An approach to systematically update finite state protocols while preserving application independent properties such as consistency and executability is described. Protocols are modelled as a network of communicating finite state machines with each machine denoting the behavior of a single protocol controller. Updates to protocols are specified as a finite set of rules that may add, delete and/or replace one or more transitions in one or more controllers. Conditions on updates are identified under which a single transition in a single controller or multiple transitions in one or more controllers can be changed to produce an executable protocol with a consistent global transition relation. The effectiveness of the proposed approach is illustrated on a large class of cache coherence protocols. It is shown how several common design choices can be consistently incorporated into these protocols by specifying them as updates. Many changes to verified protocols are non-monotonic in the sense that they do not preserve all of the verified protocol invariants. The proposed approach enables incremental verification of application independent properties that need to be preserved by any update and are a precursor to verification of the application specific properties.

Original languageEnglish (US)
Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
EditorsJim Davies, Wolfram Schulte, Mike Barnett
PublisherSpringer Verlag
Pages341-356
Number of pages16
ISBN (Electronic)3540238417, 9783540238416
DOIs
StatePublished - 2004

Publication series

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

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'An approach to preserve protocol consistency and executability across updates'. Together they form a unique fingerprint.

  • Cite this

    Subramaniam, M., & Chundi, P. (2004). An approach to preserve protocol consistency and executability across updates. In J. Davies, W. Schulte, & M. Barnett (Eds.), Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (pp. 341-356). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 3308). Springer Verlag. https://doi.org/10.1007/978-3-540-30482-1_30