A Compositional Framework for Symbolic Simulation and Formal Analysis of Network Protocols

José Meseguer, Ambarish Sridharanarayanan and Carolyn Talcott.

This work is supported by the DARPA FTN Project Composable Formal Models for High-Assurance Fault Tolerant Networks.

Formal modelling and executable specification of network protocols can provide great insight into potential flaws in the design or an implementation. Till date, such modelling has been carried out by specifying each protocol as well as its behaviour in an ad hoc manner. This is an attempt to build a standard framework for specifying such protocols in rewriting logic.

We have used the Maude language and system for scalably implementing the framework in the form of a network simulator. Maude is theoretically founded on rewriting logic, and allows for executable specification as well as model-checking. The framework thus allows both execution of protocols and systems specified as well as model-checking and proving properties about them.

The current state of the specification can be found below; please note that it is a snapshot of a work in progress and as such incomplete in some aspects.

Relevant References:

  1. M. Clavel, F. Duran, S. Eker, P. Lincoln, N. Martí-Oliet, J. Meseguer and C. Talcott: The Maude 2.0 System. In Robert Nieuwenhuis, editor, Rewriting Techniques and Aplications, volume 2706 in Lecture Notes in Computer Science, pp. 76-87. Springer-Verlag, 2003.
  2. Narciso Martí-Oliet and José Meseguer: Rewriting logic as a logical and semantic framework. In J. Meseguer, editor, Electronic Notes in Theoretical Computer Science, Vol. 4, Elsevier Science Publishers, 2000.
  3. Manuel Clavel, Francisco Durán, Steven Eker, Patrick Lincoln, Narciso Martí-Oliet, José Meseguer and José F. Quesada: Maude: Specification and Programming in Rewriting Logic. In Theoretical Computer Science, 2001.
  4. Steven Eker, José Meseguer and Ambarish Sridharanarayanan: The Maude LTL Model Checker. In Fabio Gadducci and Ugo Montanari, editors, Proceedings of Fourth Workshop on Rewriting Logic and its Applications, WRLA '02, volume 71 of Electronic Notes in Theoretical Computer Science, Elsevier, 2002.

The formal specification in Maude 2.1 with Full Maude 2.1 (available for download at the Maude web-page) can be found here.

The package contains:

Ambarish Sridharanarayanan