Pragmatics Annotated Coloured Petri Nets for Protocol Software Generation and Verification

摘要

Pragmatics Annotated Coloured Petri Nets (PA-CPNs) are a restricted class of Coloured Petri Nets (CPNs) developed to support automated generation of protocol software. The practical application of PA-CPNs and the supporting PetriCode software tool have been discussed and evaluated in earlier papers already. The contribution of this paper is to give a formal definition of PA-CPNs, motivate the definitions, and demonstrate how the structure of PA-CPNs can be exploited for more efficient verification.