A uniform deductive approach for parameterized protocol safety

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.