Pragmatics Annotated Coloured Petri Nets for Protocol Software Generation and Verification

Kent Inge Fagerland Simonsen, Lars Michael Kristensen, Ekkart Kindler

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

263 Downloads (Pure)

Abstract

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). Petri-Code 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.
Original languageEnglish
Title of host publicationProceedings of the International Workshop on Petri Nets and Software Engineering (PNSE'15) : including the International Workshop on Petri Nets for Adaptive Discrete Event Control Systems (ADECS 2015)
EditorsDaniel Moldt, Heiko Rölke, Harald Störrle
Publication date2015
Pages79-98
Publication statusPublished - 2015
EventInternational Workshop on Petri Nets and Software Engineering 2015 - Brussels, Belgium
Duration: 22 Jun 201523 Jun 2015
Conference number: 36/15
http://www.informatik.uni-hamburg.de/TGI/events/pnse15/

Workshop

WorkshopInternational Workshop on Petri Nets and Software Engineering 2015
Number36/15
CountryBelgium
CityBrussels
Period22/06/201523/06/2015
OtherA satellite event of Petri Nets 2015 and ACSD 2015
Internet address
SeriesCEUR Workshop Proceedings
Volume1372
ISSN1613-0073

Fingerprint 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