Modeling and Verification of End-to-End Protocols
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.
KeywordsContext Variable Output Location Transport Protocol Internal Event Virtual Link
Unable to display preview. Download preview PDF.
- 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.H. Kawashima, K. Futami, and S. Kand, “Functional Specification of Call Processing by State Transition Diagrams”,Google Scholar
- IEEE Trans. Comm. Tech., Vol. COM-19, October 1971, pp. 581–587.Google Scholar
- 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
- 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
- 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.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
- 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.R. C. Chen, “Representation of Process Synchronization”, Proa, of the ACM SIGCOMM/SIGOPS Interprocess Communications Workshop 1975.Google Scholar
- 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.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
- 16.N.V. Stenning, “A Data Transfer Protocol”, Computer Networks. Vol. 1, N° 2, September 1976, pp. 99–110.Google Scholar
- 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
- 18.J. Hajek, “Automatically verified Data Transfer Protocols”, Proa. Int. Comp. Comm. Conf., Kyoto, September 1978, pp. 749–756.Google Scholar
- 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
- 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
- 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
- 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
- 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.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
- 26.R.M. Keller, “Formal Verification of Parallel Programs”, CACM, 7, 1976, pp. 371–384.Google Scholar
- 27.C. Sunshine, “Formal Techniques for Protocol Specification and Verification”, IEEE Computer Magazine, August 1979, 21 p.Google Scholar
- 26.C.A. Sunshine, “Survey of Protocol Definition and Verification Techniques”, Proc. Computer Network Protocols Symposium, Univ. of Liège, February 1978.Google Scholar