A uniform deductive approach for parameterized protocol safety

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.

REFERENCES

• 1: K. Baukus, Y. Lakhnech, and K. Stahl. Verification of Parameterized Protocols. Journal of Universal Computer Science, 7(2):141--158, 2001.
• 2: J.-F. Couchot and A. Giorgetti. Analyse d'atteignabilité déductive. In Congrés Approches Formelles dans l'Assistance au Développement de Logiciels, AFADL'04, pages 269--283, 2004.
• 3: Giorgio Delzanno , Tevfik Bultan, Constraint-Based Verification of Client-Server Protocols, Proceedings of the 7th International Conference on Principles and Practice of Constraint Programming, p.286-301, November 26-December 01, 2001
• 4: Giorgio Delzanno , Javier Esparza , Andreas Podelski, Constraint-Based Analysis of Broadcast Protocols, Proceedings of the 13th International Workshop and 8th Annual Conference of the EACSL on Computer Science Logic, p.50-66, September 20-25, 1999
• 5: G. Delzanno and A. Podelski. Constraint-based deductive model checking. Int. Journal on Software Tools for Technology Transfer, 3(3):250--270, 2001.
• 6: P. Fontaine and E. P. Gribomont. Decidability of invariant validation for parameterized systems. In Proc. 9th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'03), volume 2619 of LNCS, pages 97--112. Springer, 2003.
• 7: Susanne Graf , Hassen Saïdi, Construction of Abstract State Graphs with PVS, Proceedings of the 9th International Conference on Computer Aided Verification, p.72-83, June 22-25, 1997
• 8: Yonit Kesten , Oded Maler , M. Marcus , Amir Pnueli , Elad Shahar, Symbolic Model Checking with Rich ssertional Languages, Proceedings of the 9th International Conference on Computer Aided Verification, p.424-435, June 22-25, 1997
• 9: T. Rybina and A. Voronkov. A logical reconstruction of reachability. In Perspectives of System Informatics, volume 2890 of LNCS, pages 222--237. Springer, 2003.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification

General Terms:
Verification

Keywords:
assertion, generalized substitutions, reachability, safety, symbolic model checking