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 language||English (US)|
|Number of pages||16|
|Journal||Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|
|Publication status||Published - Dec 1 2004|
ASJC Scopus subject areas
- Theoretical Computer Science
- Computer Science(all)