Formal specification and validation of ISO transport protocol components, using petri nets

ABSTRACT

In this paper, we provide the Petri net formal specifications of three important components of the ISO transport protocol: timeout mechanism, data transfer phase and connection establishment and release phases. A validation of these component Petri net specifications is then presented, followed by a discussion of its results. The validations we conducted made use of a software tool based on OGIVE [1], which can check a given Petri net for general properties such as boundedness, properness and liveness, and designer defined structural properties using Petri net invariants. We have extended OGIVE to allow for the checking of reception errors and state ambiguities as well.

REFERENCES

• 1: B. Chezaviel-Pradin: Un outil graphique interactif pour la validation des systemes a évolution parallèle décrits par reseaux de Petri (OGIVE), Thèse de Docteur-Ingenieur, Universite Paul Sebatier, Toulouse, Dec. 1979
• 2: M, Diaz: Modeling and analysis of communication and cooperation protocols using Petri net based models, Computer Networks 6 (1982). pp. 419-441
• 3: C. A. R. Hoare, Communicating sequential processes, Communications of the ACM, v.21 n.8, p.666-677, Aug. 1978 [doi>10.1145/359576.359585]
• 4: K. Lautenbach, H. Schmid: Use of Petri nets for proving correctness of concurrent process systems, IFIP 1974. North Holland Publ., Amsterdam 1974, pp. 187-191
• 5: P. V. Studnitz: Transport Protocols: Their performance and status in international standardization (July 1982), Computer Networks 7 (1983), pp. 27-35
• 6: R. Valette. M. Diaz: Top-down formal specification and verification of parallel control systems, Digital Process, Vol 4, No. 4, 1978, pp. 181-189
• 7: S. T. Vuong, D. D. Cowan: A decomposition method for the validation structured protocols, Proceedings of INFOCOM conference. Las Vegas, April 1983, pp. 209-220
• 8: P. Zafiropulo, C. H. West, H. Rudin, D. D. Cowan, D. Brand: Towards analyzing and synthesizing protocols. IEEE Trans, on Communications, Vol. COM-28, No. 4. April 1980, pp. 651-661
• 9: DIS 7499, Data Processing Systems - Open Systems Interconnection - Basic Reference Model, Computer Networks 5(1981), pp. 81-118
• 10: ISD/TC97/SC16 N2610 (Oct. 82). Data Processing Systems - Open Systems Interconnection - Network Service Definition
• 11: DP 8073, ISO/TC97/SC16 N1169 (June 82). Data Processing Systems - Open Systems Interconnection - Transport Protocol Specification
• 12: DP 8072, ISO/TC97/SC16 N1162 (June 82). Data Processing Systems - Open Systems Interconnection - Transport Service Definition
• 13: W. Jürgensen, S. T. Vuong: Validation of ISO transport protocol parts using OGIVE, Tech. Rep., University of British Columbia, 1984
• 14: S. T. Vuong and D. D. Cowan: Automated protocol validation via resynthesis: The CCITT X.75 packet level recommendation as an example, J. of Telecommunication Networks, Summer issue, 1983
• 15: Son T. Vuong , Donald D. Cowan, Reachability analysis of protocols with FIFO channels, Proceedings of the symposium on Communications Architectures & Protocols, March 08-09, 1983, Austin, Texas
• 16: G. V. Bochmann: A general transition model for protocols and communication services, IEEE Tr. on Communications, Vol. COM-28, No. 4. April 1980

INDEX TERMS

Primary Classification:
  C. Computer Systems Organization
  C.2 COMPUTER-COMMUNICATION NETWORKS
      C.2.6 Internetworking
          Subjects: Standards (e.g., TCP/IP)

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.2 Design Tools and Techniques
          Subjects: Petri nets
      D.2.4 Software/Program Verification
          Subjects: Validation

General Terms:
Design, Verification