On compositionality and Petri nets in protocol engineering

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.