Pragmatics Annotated Coloured Petri Nets for Protocol Software Generation and Verification
Peer reviewed, Journal article
MetadataShow full item record
Original versionSimonsen KIF, Kristensen LM, Kindler E. Pragmatics Annotated Coloured Petri Nets for Protocol Software Generation and Verification. CEUR Workshop Proceedings. 2015;1372:79-98
PetriCode is a tool that supports automated generation of protocol software from a restricted class of Coloured Petri Nets (CPNs) called Pragmatics Annotated Coloured Petri Nets (PA-CPNs). PetriCode and PA-CPNs have been designed with five main requirements in mind, which include the same model being used for verification and code generation. The PetriCode approach has been discussed and evaluated in earlier papers already. In this paper, we give a formal definition of PA-CPNs and demonstrate how the specific structure of PA-CPNs can be exploited for verification purposes.