
This Article  
 
Share  
Bibliographic References  
Add to:  
Digg Furl Spurl Blink Simpy Del.icio.us Y!MyWeb  
Search  
 
ASCII Text  x  
P.W. King, "Formalization of Protocol Engineering Concepts," IEEE Transactions on Computers, vol. 40, no. 4, pp. 387403, April, 1991.  
BibTex  x  
@article{ 10.1109/12.88460, author = {P.W. King}, title = {Formalization of Protocol Engineering Concepts}, journal ={IEEE Transactions on Computers}, volume = {40}, number = {4}, issn = {00189340}, year = {1991}, pages = {387403}, doi = {http://doi.ieeecomputersociety.org/10.1109/12.88460}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }  
RefWorks Procite/RefMan/Endnote  x  
TY  JOUR JO  IEEE Transactions on Computers TI  Formalization of Protocol Engineering Concepts IS  4 SN  00189340 SP387 EP403 EPD  387403 A1  P.W. King, PY  1991 KW  design principles; formal description techniques; complexity; communication system development; communication protocols; structural models; behavioral models; Petri nets; LOTOS; relational notation; Z notation; ObjectZ; formal specification; Petri nets; protocols. VL  40 JA  IEEE Transactions on Computers ER   
A vast variety of design principles and formal description techniques (FDTs) have been advocated to help contend with the everincreasing 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 ObjectZ.
[1] M. Abadi and L. Lamport, "The existence of refinement mappings," inProc. 3rd IEEE Symp. Logic Comput. Sci. (LICS'88), 1988, pp. 165175.
[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. 141. SpringerVerlag.
[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., SpringerVerlag, 1986, pp. 120.
[4] B. Alpern and F. Schneider, "Defining liveness.Inform. Processing Lett., vol. 21, pp. 181185, 1985.
[5] D. Anderson and L. Landweber, "Protocol specification by RealTime Attribute Grammars (extended abstract)," inProtocol Specification, Testing, and Verification, IV, Y. Yemini, R. Strom, and S. Yemini, Eds., NorthHolland, 1985, pp. 457465.
[6] F. Belina and D. Hogrefe, "The CCITTspecification and description language SDL,"Comput. Networks ISDN Syst., vol. 16, no. 4, pp. 311341, 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 EstelleResults of the ESPRIT/SEDOS Project, M. Diaz, J.P. Ansart, J.P. Courtiat, P. Azema, and V. Chari, Eds. New York: NorthHolland, 1989, pp. 30332.
[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: NorthHolland, 1987, pp. 7384.
[10] D. Carrington, D. Duke, R. Duke, P. King, G. Rose, and G. Smith, "ObjectZ: An objectoriented extension to Z," inFormal Description Techniques, II (FORTE'89), S. Vuong, Ed., NorthHolland, 1990, pp. 281296.
[11] R. Casley, R.F. Crew, J. Meseguer, and V. Pratt, "Temporal structures," Tech. Rep. CSLTR89408, 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. 5973.
[13] C. Chow, M. Gouda, and S. Lam, "An exercise in constructing multiphase communication protocols," inProc. ACM SIGCOMM'84, 1984, pp. 4247.
[14] C. H. Chow, M. G. Gouda, and S. S. Lam, "A discipline for constructing multiphase communicating protocols,"ACM Trans. Comput. Syst., vol. 3, no. 4, pp. 315343, 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. 117127.
[16] COST 11 bis group on FDT/AEFSD, "An approach for evaluating formal description techniques," inProtocol Specification, Testing, and Verification, V, M. Diaz, Ed., NorthHolland, 1986, pp. 421438.
[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., NorthHolland, 1987, pp. 5370.
[18] R. De Nicola, "Extensional equivalences for transition systems.Acta Informatica, vol. 24, pp. 211237, 1987.
[19] D. Duke and R. Duke, "Toward a semantics for ObjectZ," inVDM'90: VDM and Z!, vol. 428Lect. Notes in Comput. Sci., D. Bjørner, C.A.R. Hoare, and H. Langmaack, Eds., SpringerVerlag, 1990, pp. 242262.
[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., NorthHolland, 1988, pp. 3346.
[21] R. Duke, P. King, and G. Smith, "Formalising behavioral compatibility for reactive objectoriented systems," Tech. Rep. 163, Dep. Comput. Sci., Univ. of Queensland, Australia, 1990.
[22] Ehrig, H., and B. Mahr,Fundamentals of Algebraic Specification 1, SpringerVerlag, Berlin, 1985.
[23] R. Gotzhein, "The formal definition of the architectural concept 'interaction point'," InFormal Description Techniques, II (FORTE'89), S. Vuong, Ed., NorthHolland, 1990, pp. 6781.
[24] R. Gotzhein, "Specifying communication services with temporal logic," inProtocol Specification, Testing, and Verification, X, L. Logrippo, R. Probert, and H. Ural, Eds., NorthHolland, 1990. (To appear).
[25] J. Gunawardena, "Causal automata I: Confluence≡{AND, OR} causality," InProc. BCSFACS Workshop on Semantics for Concurrency, M.Z. Kwiatkowska, M.W. Shields, and R.M. Thomas, Eds., Leicester, SpringerVerlag, July 1990, pp. 137156.
[26] I. Hayes, Ed.,Specification Case Studies (Series in Computer Science). Englewood Cliffs, NJ: PrenticeHall International, 1987.
[27] J. He, "Process simulation and refinement,"Formal Aspects of Computing, vol. 1, pp. 229241, 1989.
[28] M. Hennessy and R. Milner, "Algebraic laws for nondeterminism and concurrency,"J. ACM, vol. 32, no. 1, pp. 137161, 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. 12431252, 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, "EstelleA Formal Description Technique Based on an Extended State Transition Model," 1988. International Standard 9074.
[34] ISO TC97/SC21, "LOTOSA 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 statebased approach to communicating processes,"Distributed Comput., vol. 3, pp. 918, 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., NorthHolland, 1990, pp. 318.
[38] S. Lam and A. U. Shankar, "Specifying modules to satisfy interfaces: A state transition system approach," Tech. Rep. TR8830, 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. 755775, 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., SpringerVerlag, 1985, pp. 77122.
[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., SpringerVerlag, 1987, pp. 279324.
[43] R. Milner,A Calculus of Communicating Systems (Lecture Notes in Computer Science 92). New York: SpringerVerlag, 1980.
[44] C. Morgan,Programming from Specifications, International Series in Computer Science. Englewood Cliffs, NJ: PrenticeHall, 1990.
[45] C. Morgan and B. Sufrin, "Specification of the Unix filing system,"IEEE Trans. Software Eng., vol. SE10, no. 2, pp. 128142, 1984. (An updated version appears in [26]).
[46] S. Nash, "Format and protocol language (FAPL),"Comput. Networks ISDN Syst., vol. 14, pp. 6177, 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., SpringerVerlag, 1987, pp. 393415.
[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. 455495.
[49] J. L. Peterson,Petri Net Theory and the Modeling of Systems. Englewood Cliffs, NJ: PrenticeHall, 1981.
[50] Pratt, V., "Modeling Concurrency with Partial Orders,"Int'l J. Parallel Programming, Vol. 15, No. 1, Feb. 1986, pp. 3371.
[51] W. Reisig, "Petri nets: An introduction," inEATCS Monographs on Theoretical Computer Science. New York: SpringerVerlag, 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., NorthHolland, 1988, pp. 287298.
[53] R. Saracco and P. Tilanus, "CCITT SDL: Overview of the language and its applications,"Comput. Networks ISDN Syst., vol. 13, pp. 6574, 1987.
[54] A.U. Shankar and S. Lam, "Timedependent distributed systems: moving safety, liveness and realtime properties,"Distributed Comput., vol. 2, pp. 6179, 1987.
[55] The SPECS Consortium and J. Bruijning, "Evaluation and integration of specification languages,"Comput. Networks ISDN Sys., vol. 13, pp. 7589, 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 ZAn 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. SE8, no. 5, pp. 460489, 1982.
[59] K. Turner, "An architectural semantics for LOTOS," InProtocol Specification, Testing, and Verification, VII, H. Rudin and C. West, Eds., NorthHolland, 1987, pp. 1528
[60] R. Venkatraman and T. Piatkowski, "A formal comparison of formal protocol specification techniques," inProtocol Specification, Testing, Verification, V, M. Diaz, Ed., NorthHolland, 1986, pp. 401420.
[61] G. v. Bochmann, "Specifications of a simplified transport protocol using different formal description techniques,"Computer Networks ISDN Syst., vol. 18, pp. 335377, 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., SpringerVerlag, 1989, pp. 6180.
[63] H. Zimmermann, "OSI reference modelThe ISO model of architecture for Open Systems Interconnection,"IEEE Trans. Commun., vol. COM28, no. 4, pp. 425432, Apr. 1980.