This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Formalization of Protocol Engineering Concepts
April 1991 (vol. 40 no. 4)
pp. 387-403

A vast variety of design principles and formal description techniques (FDTs) have been advocated to help contend with the ever-increasing complexity of communication system development. However, the relationship between these principles and FDTs is unclear. The author formalizes a number of concepts relevant to the design principles and FDTs used to develop communication protocols. The concepts are divided into behavioral and structural concepts. Four behavioral models and a number of associated properties are defined as a basis for comparing and integrating FDTs. Two structural models, which extend the behavioral models, are then presented, and several structural concepts are defined in terms of these models. The models and properties defined within this framework are used to briefly characterize a number of FDTs. The representative FDTs considered here are Petri nets, LOTOS, a relational notation, the Z notation, and Object-Z.

[1] M. Abadi and L. Lamport, "The existence of refinement mappings," inProc. 3rd IEEE Symp. Logic Comput. Sci. (LICS'88), 1988, pp. 165-175.
[2] M. Abadi and L. Lamport, "Composing specifications," inProc. REX Workshop on Stepwise Refinement of Distributed Systems, Lect. Notes in Comput. Sci., J.W. de Bakker, W.-P. de Roever, and G. Rozenberg, Eds., vol. 430, 1990, pp. 1-41. Springer-Verlag.
[3] L. Aceto, R. De Nicola, and A. Fantechi, "Testing equivalences for event structures," inMathematical Models for the Semantics of Parallelism, Lect. Notes in Comput. Sci., vol. 280, M. Zilli, Ed., Springer-Verlag, 1986, pp. 1-20.
[4] B. Alpern and F. Schneider, "Defining liveness.Inform. Processing Lett., vol. 21, pp. 181-185, 1985.
[5] D. Anderson and L. Landweber, "Protocol specification by Real-Time Attribute Grammars (extended abstract)," inProtocol Specification, Testing, and Verification, IV, Y. Yemini, R. Strom, and S. Yemini, Eds., North-Holland, 1985, pp. 457-465.
[6] F. Belina and D. Hogrefe, "The CCITT-specification and description language SDL,"Comput. Networks ISDN Syst., vol. 16, no. 4, pp. 311-341, Mar. 1989.
[7] T. Bolognesi and E. Brinksma, "Introduction to the ISO Specification language LOTOS,"Computer Networks ISDN Syst., vol. 14, pp. 25- 59, 1987.
[8] T. Bolognesi and M. Caneve, "Equivalence verification: Theory, algorithms and a tool," inThe Formal Description Technique Estelle--Results of the ESPRIT/SEDOS Project, M. Diaz, J.-P. Ansart, J.-P. Courtiat, P. Azema, and V. Chari, Eds. New York: North-Holland, 1989, pp. 303-32.
[9] J. Briand, M. Fehri, L. Logrippo, and A. Obaid, "Executing LOTOS specifications," inProtocol Specification, Testing, and Verification, VI, B. Sarikaya and G. von Bochmann, Eds. New York: North-Holland, 1987, pp. 73-84.
[10] D. Carrington, D. Duke, R. Duke, P. King, G. Rose, and G. Smith, "Object-Z: An object-oriented extension to Z," inFormal Description Techniques, II (FORTE'89), S. Vuong, Ed., North-Holland, 1990, pp. 281-296.
[11] R. Casley, R.F. Crew, J. Meseguer, and V. Pratt, "Temporal structures," Tech. Rep. CSL-TR-89-408, Comput. Syst. Lab., Stanford Univ., Dec. 1989.
[12] A. Cavalli and L. Farinas del Cerro, "Specification and verification of networks protocols using temporal logic," inProc.Sixiéme Colloque Intl. sur la Programmation, Toulouse, Apr. 1984, pp. 59-73.
[13] C. Chow, M. Gouda, and S. Lam, "An exercise in constructing multi-phase communication protocols," inProc. ACM SIGCOMM'84, 1984, pp. 42-47.
[14] C. H. Chow, M. G. Gouda, and S. S. Lam, "A discipline for constructing multi-phase communicating protocols,"ACM Trans. Comput. Syst., vol. 3, no. 4, pp. 315-343, Nov. 1985.
[15] E. Clarke, "Automatic verification of finite state concurrent systems using temporal logic specifications: A practical approach," inProc. 10th ACM Symp. Princ. Programming Languages, 1983, pp. 117-127.
[16] COST 11 bis group on FDT/AEFSD, "An approach for evaluating formal description techniques," inProtocol Specification, Testing, and Verification, V, M. Diaz, Ed., North-Holland, 1986, pp. 421-438.
[17] COST 11 ter group on FDT/ABM, "Architectural and behavioral modeling in computer communication," inDistributed Processing, M. Barton, E. Dagless, and G. Reijns, Eds., North-Holland, 1987, pp. 53-70.
[18] R. De Nicola, "Extensional equivalences for transition systems.Acta Informatica, vol. 24, pp. 211-237, 1987.
[19] D. Duke and R. Duke, "Toward a semantics for Object-Z," inVDM'90: VDM and Z!, vol. 428Lect. Notes in Comput. Sci., D. Bjørner, C.A.R. Hoare, and H. Langmaack, Eds., Springer-Verlag, 1990, pp. 242-262.
[20] R. Duke, I. Hayes, P. King, and G. Rose, "Protocol specification and verification using Z," inProtocol Specification, Testing, and Verification, VIII, S. Aggarwal and K. Sabnani, Eds., North-Holland, 1988, pp. 33-46.
[21] R. Duke, P. King, and G. Smith, "Formalising behavioral compatibility for reactive object-oriented systems," Tech. Rep. 163, Dep. Comput. Sci., Univ. of Queensland, Australia, 1990.
[22] Ehrig, H., and B. Mahr,Fundamentals of Algebraic Specification 1, Springer-Verlag, Berlin, 1985.
[23] R. Gotzhein, "The formal definition of the architectural concept 'interaction point'," InFormal Description Techniques, II (FORTE'89), S. Vuong, Ed., North-Holland, 1990, pp. 67-81.
[24] R. Gotzhein, "Specifying communication services with temporal logic," inProtocol Specification, Testing, and Verification, X, L. Logrippo, R. Probert, and H. Ural, Eds., North-Holland, 1990. (To appear).
[25] J. Gunawardena, "Causal automata I: Confluence≡{AND, OR} causality," InProc. BCS-FACS Workshop on Semantics for Concurrency, M.Z. Kwiatkowska, M.W. Shields, and R.M. Thomas, Eds., Leicester, Springer-Verlag, July 1990, pp. 137-156.
[26] I. Hayes, Ed.,Specification Case Studies (Series in Computer Science). Englewood Cliffs, NJ: Prentice-Hall International, 1987.
[27] J. He, "Process simulation and refinement,"Formal Aspects of Computing, vol. 1, pp. 229-241, 1989.
[28] M. Hennessy and R. Milner, "Algebraic laws for nondeterminism and concurrency,"J. ACM, vol. 32, no. 1, pp. 137-161, Jan. 1985.
[29] C.A.R. Hoare,Communicating Sequential Processes, Prentice Hall, Englewood, N.J., 1985.
[30] D. Hoffman and R. Snodgrass, "Trace specifications: Methodology and models,"IEEE Trans. Software Eng., vol. 14, no. 9, pp. 1243-1252, Sept. 1988.
[31] ISO TC97, "Architectural Semantics for FDTs," Florence, Oct. 1989. Output of Project 1.21.44 meeting.
[32] ISO TC97, "Guidelines for the Application of Estelle, LOTOS and SDL," Dec. 1989. Proposed Draft Technical Report 10167.
[33] ISO TC97/SC21, "Estelle--A Formal Description Technique Based on an Extended State Transition Model," 1988. International Standard 9074.
[34] ISO TC97/SC21, "LOTOS--A Formal Description Technique Based on the Temporal Ordering of Observational Behavior," 1988. International Standard 8807.
[35] C.B. Jones,Systematic Software Development Using VDM, Prentice Hall Int'l, 1986.
[36] M. Josephs, "A state-based approach to communicating processes,"Distributed Comput., vol. 3, pp. 9-18, 1988.
[37] P. King and G. Smith, "Formalisation of behavioral and structural concepts for communication systems," inProtocol Specification, Testing, and Verification, X, L. Logrippo, R. Probert, and H. Ural, Eds., North-Holland, 1990, pp. 3-18.
[38] S. Lam and A. U. Shankar, "Specifying modules to satisfy interfaces: A state transition system approach," Tech. Rep. TR-88-30, Univ. of Texas at Austin, Aug. 1988. (Revised Sept. 1990).
[39] S. Lam and A. U. Shankar, "A relational notation for state transition systems,"IEEE Trans. Software Eng., vol. 16, no. 7, pp. 755-775, July 1990.
[40] L. Lamport, "An axiomatic semantics of concurrent programming languages," inProc. NATO Advanced Course on Logics and Models of Concurrent SystemsK. Apt, Ed., Springer-Verlag, 1985, pp. 77-122.
[41] The Macquarie Library,The Macquarie Concise Dictionary. The Macquarie Library Pty Ltd, Australia, second ed., 1988.
[42] A. Mazurkiewicz, "Trace theory," inAdvances in Petri Nets 1986 (part II), W. Brauer, W. Reisig, and G. Rozenberg, Eds., vol. 255,Lect. Notes in Comput. Sci., Springer-Verlag, 1987, pp. 279-324.
[43] R. Milner,A Calculus of Communicating Systems (Lecture Notes in Computer Science 92). New York: Springer-Verlag, 1980.
[44] C. Morgan,Programming from Specifications, International Series in Computer Science. Englewood Cliffs, NJ: Prentice-Hall, 1990.
[45] C. Morgan and B. Sufrin, "Specification of the Unix filing system,"IEEE Trans. Software Eng., vol. SE-10, no. 2, pp. 128-142, 1984. (An updated version appears in [26]).
[46] S. Nash, "Format and protocol language (FAPL),"Comput. Networks ISDN Syst., vol. 14, pp. 61-77, 1987.
[47] M. Nielsen, "CCS - and its relationshtp to Net theory. InAdvances in Petri Nets 1986 (part II), vol. 255Lect. Notes in Comput. Sci., W. Brauer, W. Reisig, and G. Rozenberg, Eds., Springer-Verlag, 1987, pp. 393-415.
[48] Owicki, S., and L. Lamport, "Proving Liveness Properties of Concurrent Programs,"ACM Trans. Programming Languages and Systems, Vol. 4, No. 3, July 1982, pp. 455-495.
[49] J. L. Peterson,Petri Net Theory and the Modeling of Systems. Englewood Cliffs, NJ: Prentice-Hall, 1981.
[50] Pratt, V., "Modeling Concurrency with Partial Orders,"Int'l J. Parallel Programming, Vol. 15, No. 1, Feb. 1986, pp. 33-71.
[51] W. Reisig, "Petri nets: An introduction," inEATCS Monographs on Theoretical Computer Science. New York: Springer-Verlag, 1985.
[52] A. Santos, V. Freitas, and J. Neves, "The specification and prototyping of communication protocols: From heterogeneous temporal logic to concurrent prolog," InComputer Communications Systems, A. Cerveira, Ed., North-Holland, 1988, pp. 287-298.
[53] R. Saracco and P. Tilanus, "CCITT SDL: Overview of the language and its applications,"Comput. Networks ISDN Syst., vol. 13, pp. 65-74, 1987.
[54] A.U. Shankar and S. Lam, "Time-dependent distributed systems: moving safety, liveness and real-time properties,"Distributed Comput., vol. 2, pp. 61-79, 1987.
[55] The SPECS Consortium and J. Bruijning, "Evaluation and integration of specification languages,"Comput. Networks ISDN Sys., vol. 13, pp. 75-89, 1987.
[56] J. M. Spivey,The Z Notation: A Reference Manual (Computer Science Series). Englewood Cliffs, NJ: Prentice Hall International, 1989.
[57] J. M. Spivey, "The formal semantics of Z--An overview," Research note, Programming Research Group, Oxford Univ., UK, 1990.
[58] C. Sunshine, D. Thompson, R. Erickson, S. Gerhart, and D. Schwabe, "Specification and verification of communication protocols in AFFIRM using state transition models,"IEEE Trans. Software Eng., vol. SE-8, no. 5, pp. 460-489, 1982.
[59] K. Turner, "An architectural semantics for LOTOS," InProtocol Specification, Testing, and Verification, VII, H. Rudin and C. West, Eds., North-Holland, 1987, pp. 15-28
[60] R. Venkatraman and T. Piatkowski, "A formal comparison of formal protocol specification techniques," inProtocol Specification, Testing, Verification, V, M. Diaz, Ed., North-Holland, 1986, pp. 401-420.
[61] G. v. Bochmann, "Specifications of a simplified transport protocol using different formal description techniques,"Computer Networks ISDN Syst., vol. 18, pp. 335-377, 1989/1990.
[62] J. Wing, "Specifying Avalon objects in Larch," In,TAPSOFT'89 (part II), vol. 352Lect. Notes in Comput. Sci., J. Díaz and F. Orejas, Eds., Springer-Verlag, 1989, pp. 61-80.
[63] H. Zimmermann, "OSI reference model--The ISO model of architecture for Open Systems Interconnection,"IEEE Trans. Commun., vol. COM-28, no. 4, pp. 425-432, Apr. 1980.

Index Terms:
design principles; formal description techniques; complexity; communication system development; communication protocols; structural models; behavioral models; Petri nets; LOTOS; relational notation; Z notation; Object-Z; formal specification; Petri nets; protocols.
Citation:
P.W. King, "Formalization of Protocol Engineering Concepts," IEEE Transactions on Computers, vol. 40, no. 4, pp. 387-403, April 1991, doi:10.1109/12.88460
Usage of this product signifies your acceptance of the Terms of Use.