This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
PROTEAN: A High-Level Petri Net Tool for the Specification and Verification of Communication Protocols
March 1988 (vol. 14 no. 3)
pp. 301-316

The PROTEAN protocol emulation and analysis computer aid is presented. It is based on a formal specification technique called numerical Petri nets (NPNs), and provides both graphical (color) and textual interfaces to the protocol designer. NPN specifications may be created, stored, appended to other NPNs, structured, edited, listed, displayed, and analyzed. Interactive simulation, exhaustive reachability analysis, and several directed graph analysis facilities are described. Specification languages are compared, with concentration on extended finite state machines and high-level Petri nets. Both the NPN and PROTEAN facilities are described and illustrated with a simple example. The application of PROTEAN to complex examples is mentioned briefly. Work towards a comprehensive protocol engineering workstation is also discussed.

[1] CCITT,Red Book, vols. III, VI, VII, VIII. Geneva, Switzerland: ITU, 1985.
[2] L. A. Jackson, "Special issue on systems design engineering,"British Telecom Technol. J., vol. 4, July 1986.
[3] Proc. IFIP WG6.1 Int. Workshops Protocol Specification, Testing and Verification, vols. II-VII. Amsterdam, The Netherlands: North-Holland, 1982-1987.
[4] T. F. Piatkowski, "Protocol engineering," inProc. ICC, June 1983, pp. 1328-1332.
[5] T. P. Blumer and D. P. Sidhu, "Mechanical verfication and automatic implementation of communication protocols,"IEEE Trans. Software Eng., vol. SE-12, pp. 827-843, Aug. 1986.
[6] J. Billington, "Protocol engineering and nets," inProc. Eighth European Workshop Application and Theory of Petri Nets, Zaragoza, Spain, June 1987, pp. 137-156.
[7] J. Billington, M. C. Wilbur-Ham, and M. Y. Bearman, "Automated protocol verification," inProtocol Specification, Testing and Verification, V. M. Diaz, Ed. Amsterdam, The Netherlands: Elsevier, 1986, pp. 59-70.
[8] C. Paule and H. Eckert, "The Net Simulation SYstem NESSY, summary and example," GMD, Arbeitspapiere 182, Nov. 1985.
[9] M. Antilla, H. Eriksson, J. Ikonen, R. Kujansuu, L. Ojala, and H. Tuominen, "Tools and studies of formal techniques--Petri nets and temporal logic," inProtocol Specification, Testing and Verification, III, H. Rudin and C. H. West, Eds. Amsterdam, The Netherlands: Elsevier, 1983, pp. 138-148.
[10] J. P. Courtiat, J. M. Ayache, and B. Algayres, "Petri nets are good for protocols," inACM SIGCOMM '84 Symp. Communications Architectures and Protocols, Montreal, Canada, June 1984, pp. 66-74.
[11] E. T. Morgan and R. R. Razouk, "Computer-aided analysis of concurrent systems," inProtocol Specification, Testing, and Verification, V. M. Diax, Ed. New York: North Holland, 1986, pp. 49-58.
[12] K. Jensen, "Computer tools for construction, modification and analysis of Petri nets," inAdvances in Petri Nets, Part II(Lecture Notes in Comput. Sci., vol. 255). New York: Springer-Verlag, 1986, pp. 4-19.
[13] F. Feldbrugge and K. Jensen, "Petri net tool overview 1986," inPetri Nets: Applications and Relationships to Other Models of Concurrency(LNCS, vol. 255), W. Brauer, W. Reisig, and G. Rozenberg, Eds. Berlin: Springer-Verlag, Feb. 1987, pp. 20-61.
[14] G. v. Bochmann, "Usage of protocol development tools: The result of a survey," inProtocol Specification, Testing and Verification VII. Amsterdam, The Netherlands: North-Holland, 1987, pp. 147-170.
[15] CCITT, "Recommendations Z. 100 to Z. 104: Specification and Description Language," inRed Book. Geneva; Switzerland: ITU, 1985.
[16] Australia, "Reply to questionnaire on question 2/X," CCITT Study Group X, Question 2/X, Com X--No. 16, Oct. 1985.
[17] W. Brauer, Ed.,Net Theory and Applications(LNCS, vol. 84). Berlin: Springer-Verlag, 1980.
[18] W. Reisig, "Petri nets: An introduction," inEATCS Monographs on Theoretical Computer Science. New York: Springer-Verlag, 1985.
[19] W. Brauer, W. Reisig, and G. Rozenberg, Eds.,Petri Nets: Central Models and Their Properties(Lecture Notes in Computer Science, vol. 254). Berlin: Springer-Verlag, 1987.
[20] W. Brauer, W. Reisig, and G. Rozenberg,Petri Nets: Applications and Relationships to other Models of Concurrency(Lecture Notes in Computer Science, vol. 255). Berlin: Springer-Verlag, 1987.
[21] S. Drees, D. Gomm, H. Plünnecke, W. Reisig, and R. Walter, "Bibliography of net theory," inAdvances in Petri Nets 1987, G. Rozenberg, Ed. Berlin: Springer-Verlag, Apr. 1987, pp. 309-451.
[22] W. Reisig, "Petri nets in software engineering," inPetri Nets: Applications and Relationships to Other Models of Concurrency, W. Brauer, W. Reisig, and G. Rozenberg, Eds. Berlin: Springer-Verlag, 1987, pp. 63-96.
[23] F. J. W. Symons, "Modelling and analysis of communication protocols using Numerical Petri Nets," Ph.D. dissertation, Dep. Elec. Eng. Sci., Univ. Essex, Telecommun. Syst. Group Rep. 152, May 1978.
[24] E. Best and C. Fernandez, "Notations and terminology on Petri net theory," GMD, Arbeitspapiere 195, Jan. 1986.
[25] J. L. Peterson,Petri Net Theory and the Modeling of Systems. Englewood Cliffs, NJ: Prentice-Hall, 1981.
[26] J. Billington, "Specification of the Transport Service using Numerical Petri Nets," inProtocol Specification, Testing and Verification, C. Sunshine, Ed. Amsterdam, The Netherlands: North Holland, 1982, pp. 77-100.
[27] J. Billington, "Abstract specification of the ISO Transport Service definition using labelled Numerical Petri Nets," inProtocol Specification, Testing and Verification, III, H. Rudin and C. H. West, Eds. Amsterdam, The Netherlands: Elsevier, 1983, pp. 173-185.
[28] H. J. Genrich and K. Lautenbach, "System modelling with high-level Petri nets,"Theoret. Comput. Sci., vol. 13, pp. 109-136, 1981.
[29] K. Jensen, "Coloured Petri nets and the invariant-method,"Theoret. Comput. Sci., vol. 14, pp. 317-336, 1981.
[30] R. Valk, "Self-modifying nets, a natural extension of Petri nets," inAutomata, Languages and Programming, Udine(Lecture Notes in Computer Science, vol. 62). Berlin: Springer-Verlag, 1978, pp. 464-476.
[31] E. W. Dijkstra,A Discipline of Programming. Englewood Cliffs, NJ: Prentice-Hall, 1976.
[32] G. R. Wheeler, "Numerical Petri Nets--A definition," Telecom Australia, Res. Labs. Rep. 7780, May 1985.
[33] M. C. Wilbur-Ham, "Numerical Petri Nets--A guide," Telecom Australia, Res. Labs. Rep. 7791, Sept. 1985.
[34] M. C. Wilbur-Ham, "Numerical Petri Nets: A guide--version 2," Telecom Australia Res. Labs., Switching and Signalling Branch Paper 111, Mar. 1987.
[35] I. Hayes, Ed.,Specification Case Studies (Series in Computer Science). Englewood Cliffs, NJ: Prentice-Hall International, 1987.
[36] C.A.R. Hoare,Communicating Sequential Processes, Prentice Hall, Englewood, N.J., 1985.
[37] R. Milner,A Calculus of Communicating Systems (Lecture Notes in Computer Science 92). New York: Springer-Verlag, 1980.
[38] H. Rudin and C. H. West, Eds.,Tutorial Notes, IBM Zurich Res. Lab. May 1987 (Lecture Notes from the Tutorial preceding the Seventh Int. Meeting on Protocol Specification, Testing and Verification).
[39] S. Aggarwal, R. Kurshan, and K. Sabnani, "A calculus for protocol specification and validation," inProtocol Specification, Testing and Verification, III, H. Rudin and C. H. West, Eds. Amsterdam, The Netherlands: Elsevier, 1983, pp. 19-34.
[40] S. Aggarwal, D. Barbara, and K. Z. Meth, "SPANNER: A tool for the specification, analysis, and evaluation of protocols,"IEEE Trans. Software Eng., vol. SE-13, pp. 1218-1237, Aug. 1987.
[41] S. Aggarwal, D. Barbará, and K. Meth, "Specifying and analyzing protocols with SPANNER," inIEEE Int. Conf. Communications, Toronto, Canada, 1986, pp. 556-562.
[42] C. A. Sunshine, Ed.,Communication Protocol Modeling. Dedham, MA: Artech House, 1981.
[43] Formal Methods Applied to Protocols: Literature Survey, Rep. 1 to Alvey Directorate for FORMAP Project (includes reviews of 270 papers), July 1985.
[44] M. Paul and H. Siegert, Eds.,Distributed Systems: Methods and Tools for Specification. (Lecture Notes in Computer Science, vol. 190). Berlin: Springer-Verlag, 1985.
[45] W. Bibel and K. Jantke, Eds.,Mathematical Methods of Specification and Synthesis of Software Systems 1985(Lecture Notes in Computer Science, vol. 215). Berlin: Springer-Verlag, 1986.
[46] J. de Bakker, W. de Roever, and G. Rozenberg, Eds.,Current Trends in Concurrency(Lecture Notes in Computer Science, vol. 224). Berlin: Springer-Verlag, 1986.
[47] G. Müller and R. Blanc, Eds.,Networking in Open Systems(Lecture Notes in Computer Science, vol. 248). Berlin: Springer-Verlag, 1987.
[48] F. Commoner, "Deadlocks in Petri nets," Massachusetts Computer Associates, Wakefield, Rep. CA-7206-2311, June 1972.
[49] L. Lamport, "Proving the correctness of multiprocess programs,"IEEE Trans. Software Eng., vol. SE-3, pp. 125-143, Mar. 1977.
[50] A. Pnueli, "Applications of Temporal Logic to the Specification and Verification of Reactive Systems: A Survey of CurrentTrends," inCurrent Trends in Concurrency: Overviews and Tutorials. W.-P. de Roever and G. Rozenberg, eds., Lecture Notes in Computer Science 224, Springer-Verlag, N.Y., 1986, pp. 510-584.
[51] W. Reisig, "Place/transition systems," inPetri Nets: Central Models and Their Properties, W. Brauer, W. Reisig, and G. Rozenberg, Eds. Berlin: Springer-Verlag, Feb. 1987, pp. 117-141.
[52] M. C. Wilbur-Ham and J. Billington, "A protocol emulation and analysis tool," inIREECON Int., Sydney, pp. 30-32, Sept. 1983.
[53] G. R. Wheeler, M. C. Wilbur-Ham, J. Billington, and J. A. Gilmour, "Protocol analysis using Numerical Petri Nets,"Advances in Petri Nets 1985, (Lecture Notes in Computer Science, vol. 222). Berlin: Springer-Verlag, 1986, pp. 435-452.
[54] M. C. Wilbur-Ham,PROTEAN V2. 1 User's Manual. Telecom Australia Res. Labs., Clayton, Victoria, Australia, Apr. 1987.
[55] M. Y. Bearman, M. C. Wilbur-Ham, and J. Billington, "Some results of verifying the OSI class 0 Transport Protocol," inProc. ICCC, Sydney, Nov. 1984, pp. 597-602.
[56] M. Y. Bearman, "Formal specification of the Open Systems Interconnection Transport Protocol class 2 using NPNs," CSIRONET, Tech. Rep. 25, 1986.
[57] W. A. Barrett and J. D. Couch,Compiler Construction: Theory and Practice, SRA, 1979.
[58] C. A. Vissers and L. Logrippo, "The importance of the service concept in the design of communication protocols," inProtocol Specification, Testing and Verification, V. M. Diaz, Ed. Amsterdam, The Netherlands: Elsevier, 1986, pp. 3-17.
[59] CCITT, "ISDN user-network interface data link layer specification," Draft Recommendation Q.921, Working Party XI/6, Issue 7, Jan. 1984.
[60] K. A. Bartlett, R. A. Scantlebury, and P.T. Wilkinson, "A note on reliable full-duplex transmission over half-duplex link,"Commun. ACM, vol. 12, no. 5, May 1969.
[61] M. Y. Bearman, M. C. Wilbur-Ham, and J. Billington, "A formal specification of the OSI Class 0 Transport Protocol using NPNs," Telecom Australia, Victoria, Australia, Res. Lab. Rep. 7736, Oct. 1984.
[62] M. Y. Bearman, M. C. Wilbur-Ham, and J. Billington, "Analysis of Open Systems Interconnection Transport Protocol Standard,"Electron. Lett., vol. 21, pp. 659-661, July 1985.
[63] N. Kim, "Protocol analysis of signalling system no. 7 level 3," Telecom Australia, Victoria, Australia, Res. Lab. Rep. 7652, 1985.
[64] R. J. Fone, "Specification of level three of Australian ISDN primary rate access interface using Numerical Petri Nets," Draft Telecom Australia Res. Lab. Rep., July 1987.
[65] R. J. Fone, "Verification of level three of the Australian ISDN primary rate access interface using PROTEAN," Draft Telecom Australia Res. Lab. Rep., July 1987.
[66] R. J. Fone, "Inconsistencies between X.212 and Q.920-Q.921," submitted to CCITT WP VII/5, Q.43, May 1986.
[67] R. J. Fone, "Another sequence of primitives in X.212," submitted to CCITT WP VII/5, Q.43, Sept. 1986.
[68] B. Baumgarten, P. Ochsenschläger, and R. Prinoth, "Building blocks for distributed system design," inProtocol Specification, Testing and Verification, V, M. Diaz, Ed. Amsterdam, The Netherlands: Elsevier, 1986, pp. 19-38.
[69] G. Berthelot, "Transformations and decompositions of nets," inPetri Nets: Central Models and Their Properties, W. Brauer, W. Reisig, and G. Rozenberg, Eds. Berlin: Springer-Verlag, 1987, pp. 359- 376.
[70] J. Katzenelson and R. Kurshan, "S/R: A language for specifying protocols and other coordination processes," inProc. Fifth Annu. Phoenix Conf. Computers and Communications '86, Washington, Mar. 1986, pp. 286-292.
[71] H. Tuominen, "Temporal logic as a query language for Petri net reachability graphs," inSeventh European Workshop Application and Theory of Petri Nets, July 1986.
[72] E. M. Clarke, E. A. Emerson, and A. P. Sistla, "Automatic verification of finite-state concurrent systems using temporal logic,"ACM Trans. Program. Lang. Syst., vol. 8, no. 2, pp. 244-263, Apr. 1986.
[73] M. C. Browne, "An improved algorithm for the automatic verification of finite state systems using temporal logic," inProc. 1986 Conf. Logic Computer Science, Cambridge, MA, June 1986, pp. 260-267.
[74] K. Jensen, "Colored Petri nets," inPetri Nets: Central Models and Their Properties, W. Brauer, W. Reisig, and G. Rozenberg, Eds. Bad Honnef, W. Germany: Springer-Verlag, 1987, pp. 248-299.
[75] E. Clarke, O. Grümberg, and M. C. Browne, "Reasoning about networks with many identical finite-state processes," inProc. Fifth Annu. ACM Symp. Principles of Distributed Computing, Aug. 1986, pp. 240-248.
[76] K. Lautenbach and H. Schmid, "Use of Petri nets for proving correctness of concurrent process systems," inProc. IFIP Congress. Amsterdam, The Netherlands: North-Holland, 1974, pp. 187-191.
[77] G. Memmi and G. Roucairol, "Linear algebra in net theory," inNet Theory and Applications, W. Brauer, Ed. Berlin: Springer-Verlag, 1980.
[78] G. Memmi and J. Vautherin, "Analyzing nets by the invariant method," inPetri Nets: Central Models and Their Properties, W. Brauer, W. Reisig, and G. Rozenberg, Eds. Berlin: Springer-Verlag, 1987, pp. 300-336.
[79] H. J. Genrich and K. Lautenbach, "The analysis of distributed systems by means of predicate/transition nets," inSemantics of Concurrent Computation, G. Kahn Ed. New York: Springer-Verlag, 1979, pp. 123-146; also in Lect. Notes in Computer Sciences, vol. 70.
[80] T. J. Batten, "An extension to invariants analysis techniques applied to Petri net models of protocols," Sept. 1986,Australian Telecommun. Res., to be published.
[81] G. Winskel, "Petri nets, algebras and morphisms," Univ. Cambridge Comput. Lab., Tech. Rep. 79, Sept. 1985.
[82] G. J. Holzmann, "On limits and possibilities of automated protocols analysis," inIFIP WC-6.1 7th Int. Conf. Protocol Specification, Testing and Verification. North Holland, 1987.
[83] International Workshop on Timed Petri Nets, IEEE Comput. Soc., Torino, Italy, July 1985.
[84] R. Razouk and C. Phelps, "Performance analysis using timed Petri nets," inProtocol Specification, Testing and Verification, IV, Y. Yemini, R. Strom, and S. Yemini, Eds. Amsterdam, The Netherlands: Elsevier, 1985.
[85] International Workshop on Petri Nets and Performance Models, IEEE Comput. Soc., Madison, WI, Aug. 24-26, 1987.

Index Terms:
graphical interfaces; interactive simulation; specification languages; PROTEAN; high-level Petri net tool; specification; verification; communication protocols; numerical Petri nets; textual interfaces; exhaustive reachability analysis; directed graph analysis; finite state machines; engineering workstation; directed graphs; finite automata; protocols; software tools
Citation:
J. Billington, G.R. Wheeler, M.C. Wilbur-Ham, "PROTEAN: A High-Level Petri Net Tool for the Specification and Verification of Communication Protocols," IEEE Transactions on Software Engineering, vol. 14, no. 3, pp. 301-316, March 1988, doi:10.1109/32.4651
Usage of this product signifies your acceptance of the Terms of Use.