Composable Coloured Petri Nets with Protocol Modeling Semantics

Abstract. We define a modeling language based on combining Coloured Petri Nets with Protocol Modeling semantics. This language combines the expressive power of Coloured Petri Nets in describing behavior with the ability provided by Protocol Modeling to compose partial behavioral descriptions. The resultant language can be considered as a domain spe-cific Coloured Petri Net based language for deterministic and constantly evolving systems. We show that the composition used in Protocol Modeling guarantees preservation of the behavior of composed parts, and hence supports local reasoning about the behavior of the whole based on examination of the composed parts. We present the proof of this key property in this paper. We describe the modifications required to conventional Coloured Petri Net semantics to incorporate Protocol Modeling ideas, and show that they are minimal. The advantages of incorporating Protocol Modeling semantics are significant and promise to improve the usability and prac-ticality of Petri Net based modeling. We illustrate these advantages using examples