Petri nets are good for protocols

ABSTRACT

This paper is intended to survey the applicability of Petri nets for protocol, as well as for service specification and validation. At the specification level, different classes of nets are introduced, and emphasis is given to the modular specification of a protocol layer. At the validation level, the analysis techniques implemented in the CAD package OGIVE/OVIDE are presented, and are used in order to prove safety and progress properties of a protocol layer. Finally, the specification and validation of the ISO Transport protocol is chosen as a significant example of the proposed design methodology.

REFERENCES

• 1: G.V. Bochmann, "A general transition model for protocols and communication services", IEEE Trans. on Comm., April 1980.
• 2: R.L. Schwartz, P.M. Melliar-Smith, "From state machines to temporal logic: specification methods for protocol standards", IEEE Trans. on Comm., December 1982.
• 3: C.A. Sunshine et al, "Specification and verification of communication protocols in AFFIRM using state-transition models", IEEE Trans. on Software Engineering, September 1982.
• 4: M. Diaz, "Modeling and analysis of communication and cooperation protocols using Petri net based models", Computer Networks, December 1982.
• 5: B. Montel et al, "OVIDE, a software package for the validation of systems represented by Petri net based models", |4th European Workshop on Applications and Theory of Petri nets,# Toulouse, September 1983.
• 6: H. Zimmermann, "OSI reference model, the ISO model of architecture for open systems interconnection", IEEE.Trans. on Comm., April 1980.
• 7: B. Berthomieu, M. Menasche, "An enumerative approach for analysing time Petri nets", Proceedings of IFIP, 1983, Paris.
• 8: L. Logrippo, "Constructive and executable specifications of protocol services by using abstract data types and finite state transducers", Proceedings of the IFIP WG 6.1. Third Int. Workshop on Protocol Specification, Testing and Verification, Z(@@@@)rich, June 1983.
• 9: B. Algayres, "Sur la modélisation, la validation et l'implémentatio d'un protocole de transport", Docteur-Ingénieur Thesis, Toulouse, 1982.
• 10: J. Billington, "Abstract specification of the ISO transport service definition using labelled numerical Petri nets", Proceedings of the IFIP WG 6.1. Third Int. Workshop on Protocol Specification, Testing and Verification, Z(@@@@)rich, June 1983.
• 11: J.M. Ayache, J.P. Courtiat, M. Diaz, "REBUS: a fault tolerant distributed system for industrial real-time control", IEEE Trans. on Computers, Special Issue on Fault Tolerant Computing, July 1982.
• 12: B.T. Hailpern, S.S. Owicki, "Modular verification of computer communication protocols", IEEE Trans. on Comm. January 1983.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.2 Design Tools and Techniques
          Subjects: Petri nets

Additional Classification:
  C. Computer Systems Organization
  C.2 COMPUTER-COMMUNICATION NETWORKS
      C.2.2 Network Protocols
  C.4 PERFORMANCE OF SYSTEMS
      Subjects: Reliability, availability, and serviceability

General Terms:
Design, Performance, Reliability

Keywords:
ISO reference model, Petri nets, Protocol, Service, Specification, Validation