Pragmatics Annotated Coloured Petri Nets for Protocol Software Generation and Verification

Kent Inge  Fagerland Simonsen; Lars Michael Kristensen; Ekkart Kindler

Pragmatics Annotated Coloured Petri Nets for Protocol Software Generation and Verification

Kent Inge Fagerland Simonsen, Lars Michael Kristensen, Ekkart Kindler

Department of Applied Mathematics and Computer Science

Western Norway University of Applied Sciences

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

403 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 language	English
Title of host publication	Proceedings 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)
Editors	Daniel Moldt, Heiko Rölke, Harald Störrle
Publication date	2015
Pages	79-98
Publication status	Published - 2015
Event	International Workshop on Petri Nets and Software Engineering 2015 - Brussels, Belgium Duration: 22 Jun 2015 → 23 Jun 2015 Conference number: 36/15 http://www.informatik.uni-hamburg.de/TGI/events/pnse15/

Workshop

Workshop	International Workshop on Petri Nets and Software Engineering 2015
Number	36/15
Country/Territory	Belgium
City	Brussels
Period	22/06/2015 → 23/06/2015
Other	A satellite event of Petri Nets 2015 and ACSD 2015
Internet address	http://www.informatik.uni-hamburg.de/TGI/events/pnse15/

Series	CEUR Workshop Proceedings
Volume	1372
ISSN	1613-0073

Access to Document

Paper5Final published version, 785 KB

OpenUrl availability

Full text

Cite this

Fagerland Simonsen, K. I., Kristensen, L. M., & Kindler, E. (2015). Pragmatics Annotated Coloured Petri Nets for Protocol Software Generation and Verification. In D. Moldt, H. Rölke, & H. Störrle (Eds.), Proceedings 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) (pp. 79-98). CEUR Workshop Proceedings Vol. 1372

Fagerland Simonsen, Kent Inge ; Kristensen, Lars Michael ; Kindler, Ekkart. / Pragmatics Annotated Coloured Petri Nets for Protocol Software Generation and Verification. Proceedings 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). editor / Daniel Moldt ; Heiko Rölke ; Harald Störrle. 2015. pp. 79-98 (CEUR Workshop Proceedings, Vol. 1372).

@inproceedings{2d6a047448b146b8baafd81a526c2420,

title = "Pragmatics Annotated Coloured Petri Nets for Protocol Software Generation and Verification",

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.",

author = "{Fagerland Simonsen}, {Kent Inge} and Kristensen, {Lars Michael} and Ekkart Kindler",

year = "2015",

language = "English",

series = "CEUR Workshop Proceedings",

publisher = "CEUR-WS",

pages = "79--98",

editor = "Moldt, {Daniel } and R{\"o}lke, {Heiko } and St{\"o}rrle, {Harald }",

booktitle = "Proceedings of the International Workshop on Petri Nets and Software Engineering (PNSE'15)",

note = "International Workshop on Petri Nets and Software Engineering 2015, PNSE'15 ; Conference date: 22-06-2015 Through 23-06-2015",

url = "http://www.informatik.uni-hamburg.de/TGI/events/pnse15/",

}

Fagerland Simonsen, KI, Kristensen, LM & Kindler, E 2015, Pragmatics Annotated Coloured Petri Nets for Protocol Software Generation and Verification. in D Moldt, H Rölke & H Störrle (eds), Proceedings 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). CEUR Workshop Proceedings, vol. 1372, pp. 79-98, International Workshop on Petri Nets and Software Engineering 2015, Brussels, Belgium, 22/06/2015.

Pragmatics Annotated Coloured Petri Nets for Protocol Software Generation and Verification. / Fagerland Simonsen, Kent Inge ; Kristensen, Lars Michael; Kindler, Ekkart.
Proceedings 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). ed. / Daniel Moldt; Heiko Rölke; Harald Störrle. 2015. p. 79-98 (CEUR Workshop Proceedings, Vol. 1372).

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

TY - GEN

T1 - Pragmatics Annotated Coloured Petri Nets for Protocol Software Generation and Verification

AU - Fagerland Simonsen, Kent Inge

AU - Kristensen, Lars Michael

AU - Kindler, Ekkart

N1 - Conference code: 36/15

PY - 2015

Y1 - 2015

N2 - 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.

AB - 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.

UR - http://ceur-ws.org/Vol-1372/

M3 - Article in proceedings

T3 - CEUR Workshop Proceedings

SP - 79

EP - 98

BT - Proceedings of the International Workshop on Petri Nets and Software Engineering (PNSE'15)

A2 - Moldt, Daniel

A2 - Rölke, Heiko

A2 - Störrle, Harald

T2 - International Workshop on Petri Nets and Software Engineering 2015

Y2 - 22 June 2015 through 23 June 2015

ER -

Fagerland Simonsen KI, Kristensen LM, Kindler E. Pragmatics Annotated Coloured Petri Nets for Protocol Software Generation and Verification. In Moldt D, Rölke H, Störrle H, editors, Proceedings 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). 2015. p. 79-98. (CEUR Workshop Proceedings, Vol. 1372).

Pragmatics Annotated Coloured Petri Nets for Protocol Software Generation and Verification

Abstract

Workshop

Access to Document

OpenUrl availability

Other files and links

Fingerprint

Cite this