On compositionality and Petri nets in protocol engineering

  • N. A. Anisimov
  • M. Koutny
Part of the IFIP Advances in Information and Communication Technology book series (IFIPAICT)


This paper addresses the problem of designing communication protocols within the Petri net approach. Some recent results in combining Petri nets and compositionality are presented, and we argue that it should be possible to exploit these for protocol engineering. We outline a systematic approach to the design of protocol systems. At the top level, we use Petri net entities together with a set of operations. The external behaviour of entities is characterised using the notion of a bisimulation equivalence. At a lower level of design, we show how entities can be constructed from protocol procedures using suitable composition rules. The relationship between syntactic and behavioural notions of compositionality is also discussed.


Communication protocols protocol engineering Petri nets Compositionality protocol hierarchy bisimulation equivalence 


  1. Anisimov, N.A. (1989) A Notion of Petri Net Entity for Communication Protocol Design. Report, Institute for Automation and Control Processes, Russian Academy of Sciences, Vladivostok.Google Scholar
  2. Anisimov, N.A. (1991a) An Algebra of Regular Macronets for Formal Specification of Communication Protocols. Computers and Artificial Intelligence 10, 541–560.MathSciNetzbMATHGoogle Scholar
  3. Anisimov, N.A. (1991b) A Petri Net Entity as a Formal Model for LOTOS, a Specification Language for Distributed and Concurrent Systems. In: Parallel Computing Techno-logies (ed. N.N.Mirenkov), World Scientific, 440–450.Google Scholar
  4. Anisimov, N.A., Kovalenko, A.A. and Postupalski, P.A. (1993) Two—Levels Formal Model for Protocol Specification Based on Petri Nets. In: Network Information Processing Systems. Proc. of the IFIP TC6 Int. Symp. (ed. K.Boyanov), Bulgarian Academy of Sciences, 143–154.Google Scholar
  5. Baeten, J.C.M. and Weijland, W.P. (1990) Process Algebra. Cambridge Tracts in Theoretical Computer Science.Google Scholar
  6. Barbeau, M., Bochmann, G.V. (1993) A Subset of Lotos with the Computational Power of Place/Transition—Nets. In: Proc. of 14th Int. Conf. Application and Theory of Petri Nets, (ed. M.Ajmone Marsan), Springer-Verlag Lecture Notes in Computer Science 691, Springer.Google Scholar
  7. Best, E., Devillers, R. and Hall, J.G. (1992) The Box Calculus: a New Causal Algebra with Multi-label Communication. In: Advances in Petri Nets 1992, Springer-Verlag Lecture Notes in Computer Science 609, 21–69.MathSciNetCrossRefGoogle Scholar
  8. Best, E. and Hopkins, R.P. (1993) B(PN)2–a Basic Petri Net Programming Notation. Proc. of PARLE-93, Springer-Verlag Lecture Notes in Computer Science 694, 379–390.CrossRefGoogle Scholar
  9. Billington, J., Wheeler, G.H. and Wilbur-Ham, H.C. (1988) PROTEAN: A High-level Petri Net Tool for the Specification and Verification of Communication Protocols. IEEE Trans. Soft. Eng. 14, 301–315.CrossRefGoogle Scholar
  10. v.Bochmann, G. (1989/90) Specification of a Simplified Transport Protocol Using Different Formal Description Techniques. Computer Network and ISDN Systems 18, 335–377.CrossRefGoogle Scholar
  11. Bolognessi, T. and Brinksma, E. (1987) Introduction to the (ISO, 1993) Specification Language LOTOS. Computer Network and ISDN Systems 14, 25–29.CrossRefGoogle Scholar
  12. Budkowski, S. and Dembinski, P. (1987) An Introduction to Estelle: A Specification Language for Distributed Systems. Computer Network and ISDN Systems 14, 3–23.CrossRefGoogle Scholar
  13. Diaz, M. (1982) Modeling and Analysis of Communication and Cooperation Protocols Using Petri Net Based Models. Computer Networks 6, 419–441.zbMATHGoogle Scholar
  14. Diaz, M. (1987) Petri Net Based Models in the Specification and Verification of Protocols. Springer-Verlag Lecture Notes in Computer Science 255, 135–170.CrossRefGoogle Scholar
  15. Godefroid, P. and Wolper, P. (1993) Partial-order Methods for Temporal Verification. In: Proc. of Proc. Concur’93, Springer-Verlag Lecture Notes in Computer Science 715, 233–246.MathSciNetGoogle Scholar
  16. ISO (1983), IS 7498, Information Processing Systems - Open System Interconnections - Basic reference Model.Google Scholar
  17. Kotov, V.E. (1978) An Algebra for Parallelism Based on Petri Nets. Springer-Verlag Lecture Notes in Computer Science 64, 39–55.MathSciNetCrossRefGoogle Scholar
  18. Koutny, M. (1994) Partial Order Semantics of Box Expressions. In: Proc. of 15th International Conference on Application and Theory of Petri Nets, Springer-Verlag Lecture Notes in Computer Science 815, 318–337.MathSciNetGoogle Scholar
  19. Koutny, M., Best, E. and Esparza, J. (1994) Operational Semantics for the Petri Box Calculus. In: Proc. of 4th International Conference on Concurrency Theory, Springer-Verlag Lecture Notes in Computer Science 836, 210–225.MathSciNetGoogle Scholar
  20. Koutny, M. (1995) Compositional Definitions of Petri Nets. A manuscript.Google Scholar
  21. Merlin, P.M. (1976) A Methodology for The Design and Implementation of Communication Protocols. IEEE Trans. Commun. 24, 614–621.MathSciNetCrossRefGoogle Scholar
  22. Milner, R. (1989) Communication and Concurrency. Prentice Hall.zbMATHGoogle Scholar
  23. Olderog, E.R. (1987) Operational Petri Net Semantics for CCSP. In: Advances in Petri Nets 1987 (ed. G. Rozenberg), Springer-Verlag Lecture Notes in Computer Science 266, 196–223.MathSciNetCrossRefGoogle Scholar
  24. Rudin, H. (1987) Network Protocols and Tools to Help Produce Them. In: Ann. Rev. Comput. Sci. 2, 291–316.CrossRefGoogle Scholar
  25. Valmari, A. (1990) A Stubborn Attack on State Explosion. Computer-Aided Verification, AMS-ACM DIMACS Series in Discrete Mathematics and Theoretical Computer Science 3 American Mathematical Society, 25–41.MathSciNetGoogle Scholar
  26. Vissers, C.A., Scollo, G. and Van Sinderen, M. (1988) Architecture and Specification Style in Formal Description of Distributed Systems. In: Proc. of PSTV VIII (eds. S.Aggarval and K.Sabnani ), North—Holland.Google Scholar
  27. Vuong, S.T. and Cowan, D.D. (1982) A Decomposition Method for the Validation of Structured Protocols. In: Proc. of INFOCOM’82, 209–220.Google Scholar

Copyright information

© IFIP International Federation for Information Processing 1996

Authors and Affiliations

  • N. A. Anisimov
    • 1
  • M. Koutny
    • 2
  1. 1.Inst. for Automation and Control ProcessesRussian Academy of SciVladivostokRussia
  2. 2.Department of Computing ScienceUniversity of Newcastle upon TyneNewcastle upon TyneUK

Personalised recommendations