Modeling and Verification of End-to-End Protocols

  • André Danthine
Part of the Nato Advanced Study Institutes Series book series (ASIC, volume 80)


Using a simple interface protocol as example, finite state automaton and Petri nets are introduced and compared. The concept of an interface machine is discussed and rejected. The problems related to the transmission medium are introduced.

Hierarchical decomposition of computer networks into layers introduced the concept of end-to-end protocols. Such a protocol requests a global model which includes two local models and a transmission medium model. But the local model must be revisited in order to be usable in practical situation. The state variables of an automaton are supplemented by context variables. For Petri nets, predicates are introduced.

After a detailled comparison of these expanded models, the verification problem is introduced and illustrated with one example.


Context Variable Output Location Transport Protocol Internal Event Virtual Link 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    D. Bjorner, “Finite State Automaton — Definition of Data Communication Line Control Procedures”, AFIPS Proa., Vol. 37, FJCC, Houston, November 1970, pp. 477–491.Google Scholar
  2. 2.
    H. Kawashima, K. Futami, and S. Kand, “Functional Specification of Call Processing by State Transition Diagrams”,Google Scholar
  3. IEEE Trans. Comm. Tech., Vol. COM-19, October 1971, pp. 581–587.Google Scholar
  4. 3.
    R. E. Rusbridge, and A. Langsford, “Formal Representation of Protocols for Computer Networks”, Report AFRE-R-7826, UKAEA, Harwell, England, December 1974, 20 p.Google Scholar
  5. 4.
    A. A. S. Danthine, and J. J. Bremer, “An Axiomatic Description of the Transport Protocol of Cyclades”, Rechnernetze und Datenfernverarbeitung, Aachen 1976, Springer-Verlag, pp.259–273.Google Scholar
  6. 5.
    G. V. Bochmann, “Finite State Description of Communication Protocols”, Proa. Computer Network Protocole Symposium, Univ. df Liège, February 1978, pp. F3–1 to F3–11 and Computer Networks, 2, 4 /5, October 1978, pp. 361–372.Google Scholar
  7. 6.
    R. W. Stutzman, “Data Communication Control Procedures”, Comput. Surv., Vol.4, N° 4, December 1972, pp. 197–220.CrossRefGoogle Scholar
  8. 7.
    A. A. S. Danthine, and J. J. Bremer, “Communication Protocols in a Network Context”, Proa. ACM Interprocess Comm. Workshop, Santa Monica, March 1975, pp. 87–92.Google Scholar
  9. 8.
    A. A. S. Danthine, and J. J. Bremer, “Modelling and Verification of End-to-End Protocols”, SART 77/11/13, Third European Network User’s Workshop, IIASA, Laxenburg, Austria, April 19–20 1977, 17 p.Google Scholar
  10. 9.
    J. L. Peterson, “Petri nets”, ACM Computing Surveys, Vol. 9, N° 3, September 1977, pp. 223–251.MATHCrossRefGoogle Scholar
  11. 10.
    R. C. Chen, “Representation of Process Synchronization”, Proa, of the ACM SIGCOMM/SIGOPS Interprocess Communications Workshop 1975.Google Scholar
  12. 11.
    P. M. Merlin, “A Methodology for the Design and Implementation of Communication Protocols”, IEEE Trans. Corrm., Vol.COM-24, N° 5, June 1976, pp. 614–621.MathSciNetCrossRefGoogle Scholar
  13. 12.
    P.M. Merlin, and D.J. Farber, “Recoverability of Communication Protocols. Implications of a Theorical Study”, IEEE Trans. Corrm., Vol. COM-24, N° 9, September 1976, pp. 1036–1043.MathSciNetCrossRefGoogle Scholar
  14. 13.
    A. Danthine, “Petri nets for Protocol Modelling and Verification”, Proc. of the Computer Networks and Teleprocessing Symposium, Budapest, Hungary, October 1977, Vol. II, pp. 663–685.Google Scholar
  15. 14.
    P.M. Merlin, “Specification and Validation of Protocols”, IEEE Trans. Com., Vol. COM-27, pp. 1671–1680, Nov. 1979.MathSciNetCrossRefGoogle Scholar
  16. 15.
    G.V. Bochmann, “Logical Verification and Implementation of Protocols”, Proc. 4th Data Comm. Symp., Québec, October 1975, pp. 7–15 to 7–20.Google Scholar
  17. 16.
    N.V. Stenning, “A Data Transfer Protocol”, Computer Networks. Vol. 1, N° 2, September 1976, pp. 99–110.Google Scholar
  18. 17.
    D. Brand, and W. H. Joyner, “Verification of Protocols using Symbolic Execution”, Proc. Computer Network Symposium, Univ. de Liège, February 1978, pp. F2-1 to F2-7.Google Scholar
  19. 18.
    J. Hajek, “Automatically verified Data Transfer Protocols”, Proa. Int. Comp. Comm. Conf., Kyoto, September 1978, pp. 749–756.Google Scholar
  20. 19.
    J. Harangozo, “Protocol Definition with Formal Grammars”, Proc. Computer Network Protocols Symposium, Univ. of Liège, February 1978, pp. F6-1 to F6-10.Google Scholar
  21. 20.
    J.C. Day, “A Bibliography on the Formal Specification and Verification of Computer Network Protocols”, Proc. Computer Network Protocols Symposium, Univ. of Liège, February 1978Google Scholar
  22. 21.
    A.A.S. Danthine, and J.J. Bremer, “Définition, représentation et simulation de protocoles dans un contexte réseau”, Journées AIM Mini-Ordinateurs et Transmission de Données, Liège, janvier 1975, pp. 115–126.Google Scholar
  23. 22.
    A. Danthine, and J. Bremer, “Modelling and Verification of End-to-End Transport Protocols”, Proc. Computer Network Protocols Symposium, Univ. of Liège, February 1978, pp. F5-1 to F5-12 and Computer Networks, 2, 4 /5, October 1978, pp. 381–395.Google Scholar
  24. 23.
    G.J. Nutt, “Evaluation Nets for Computer System Performance Analysis”, AFIPS Conf. Proc., Vol. 41 Part 1, 1972, pp. 279–286.Google Scholar
  25. 24.
    A. Danthine, “Protocol Representation with Finite-State Models” IEEE Trans. Com., Vol. COM-28, pp. 632–643, April 1980.CrossRefGoogle Scholar
  26. 25.
    G.V. Bochmann, and J. Gecsei, “A Unified Method for the Specification and Verification of Protocols”, Proc. IFIP Congress, Toronto, 1977, pp. 229–234.Google Scholar
  27. 26.
    R.M. Keller, “Formal Verification of Parallel Programs”, CACM, 7, 1976, pp. 371–384.Google Scholar
  28. 27.
    C. Sunshine, “Formal Techniques for Protocol Specification and Verification”, IEEE Computer Magazine, August 1979, 21 p.Google Scholar
  29. 26.
    C.A. Sunshine, “Survey of Protocol Definition and Verification Techniques”, Proc. Computer Network Protocols Symposium, Univ. of Liège, February 1978.Google Scholar

Copyright information

© D. Reidel Publishing Company 1982

Authors and Affiliations

  • André Danthine
    • 1
  1. 1.Université de LiègeBelgiqueGermany

Personalised recommendations