Pragmatics Annotated Coloured Petri Nets for Protocol Software Generation and Verification

Kent Inge Simonsen, Lars Michael Kristensen, Ekkart Kindler

Research output: Book/ReportReport

472 Downloads (Pure)


This paper presents the formal definition of Pragmatics Annotated Coloured Petri Nets (PA-CPNs). PA-CPNs represent a class of Coloured Petri Nets (CPNs) that are designed to support automated code genera-tion of protocol software. PA-CPNs restrict the structure of CPN models and allow Petri net elements to be annotated with so-called pragmatics, which are exploited for code generation. The approach and tool for gen-erating code is called PetriCode and has been discussed and evaluated in earlier work already. The contribution of this paper is to give a formal def-inition for PA-CPNs; in addition, we show how the structural restrictions of PA-CPNs can be exploited for making the verification of the modelled protocols more efficient. This is done by automatically deriving progress measures for the sweep-line method, and by introducing so-called service testers, that can be used to control the part of the state space that is to be explored for verification purposes.
Original languageEnglish
Place of PublicationKgs. Lyngby
PublisherTechnical University of Denmark
Number of pages23
Publication statusPublished - 2014
SeriesDTU Compute-Technical Report-2014


Dive into the research topics of 'Pragmatics Annotated Coloured Petri Nets for Protocol Software Generation and Verification'. Together they form a unique fingerprint.

Cite this