In: Technical report No. 575, pages 1-43. Department of Computer Science, University of Newcastle upon Tyne, UK, February 1997.
Abstract: This paper addresses the problem of designing communication protocols within a framework based on Petri nets and supporting compositionality of structure and behaviour. Although Petri nets have for several years been applied as a formal model in which one could describe and analyse communication protocols, it can be argued that at present they are not widely used in protocol engineering. The main reason for this can be attributed to a lack of compositionality which meant that Petri nets were unable to deal with large computing systems. However, recent results on combining Petri nets and process algebras have radically changed that, and we here argue that Petri nets can provide an effective formal model for protocol engineering. After pointing out that compositionality is an inherent feature of protocols, and as such should be supported by adequate formal basis, we outline a systematic approach to the design of protocol systems. The top level of the design hierarchy is based on the notion of a Petri net entity and the operation of concurrent composition. The external behaviour of entities is characterised using the notion of a bisimulation equivalence. At the lower level of design, we show how entities can be constructed from protocol procedures using suitable composition rules, such as sequence, iteration and disabling. We then discuss the relationship between syntactical and semantical (behavioural) notions of compositionality.
Keywords: Communication protocols; protocol engineering.