kirancodes.me
To Proof Maintenance & Beyond!
ASE 2005

A uniform deductive approach for parameterized protocol safety

Jean-François Couchot, Alain Giorgetti, Nikolai Kosmatov

PDFDOI 10.1145/1101908.1101971dblp

Abstract

We present a uniform verification method of safety properties for classes of parameterized protocols. Properties like mutual exclusion or cache coherence are automatically verified for any number of similar processes communicating by broadcast and rendezvous. The protocols are specified in a language of generalized substitutions on array data structures. Sets of states are expressed by first-order formulae with equality. Predecessors are computed by an iterative semi-algorithm. Reaching an initial state or the fixpoint is shown to be decidable and an original decision procedure is provided. As a running example, the MESI protocol illustrates this approach. Experimental results show its applicability to various properties and protocol classes.

BibTeX
@inproceedings{Couchot-al:ASE05,
  author    = {Jean{-}Fran{\c{c}}ois Couchot and
               Alain Giorgetti and
               Nikolai Kosmatov},
  title     = {A uniform deductive approach for parameterized protocol safety},
  booktitle = {ASE},
  pages     = {364--367},
  publisher = {{ACM}},
  year      = {2005},
}

Related papers