Pragmatics Annotated Coloured Petri Nets for Protocol Software Generation and Verification
Peer reviewed, Journal article
Åpne
Permanent lenke
http://hdl.handle.net/11250/2482129Utgivelsesdato
2015Metadata
Vis full innførselSamlinger
Originalversjon
Simonsen KIF, Kristensen LM, Kindler E. Pragmatics Annotated Coloured Petri Nets for Protocol Software Generation and Verification. CEUR Workshop Proceedings. 2015;1372:79-98Sammendrag
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.
Beskrivelse
-