Code Generation for Protocols from CPN models Annotated with Pragmatics

Kent Inge Simonsen, Lars Michael Kristensen, Ekkart Kindler

Research output: Book/ReportReportResearch

278 Downloads (Pure)

Abstract

Model-driven engineering (MDE) provides a foundation for automatically generating software based on models. Models allow software designs to be specified focusing on the problem domain and abstracting from the details of underlying implementation platforms. When applied in the context of formal modelling languages, MDE further has the advantage that models are amenable to model checking which allows key behavioural properties of the software design to be verified. The combination of formally verified models and automated code generation contributes to a high degree of assurance that the resulting software implementation satisfies the properties verified for the model. Coloured Petri Nets (CPNs) have been widely used to model and verify protocol software, but limited work exists on using CPN models of protocol software as a basis for automated code generation. In this report, we present an approach for generating protocol software from a restricted class of CPN models. The class of CPN models considered aims at being descriptive in that the models are intended to be helpful in understanding and conveying the operation of the protocol. At the same time, a descriptive model is close to a verifiable version of the same model and sufficiently detailed to serve as a basis for automated code generation when annotated with code generation pragmatics. Pragmatics are syntactical annotations designed to make the CPN models descriptive and to address the problem that models with enough details for generating code from them tend to
be verbose and cluttered. Our code generation approach consists of three main steps, starting from a CPN model that the modeller has annotated with a set of pragmatics that make the protocol structure and the control-flow explicit. The first step is to compute for the CPN model, a set of derived pragmatics
that identify control-flow structures and operations, e. g., for sending and receiving packets, and for manipulating the state. In the second step, an abstract template tree (ATT) is constructed providing an association between pragmatics and code generation templates. The ATT then directs the code generation in the third step by invoking the code templates associated with each node of the ATT in order to generate code. We illustrate our approach using an example of a unidirectional data framing protocol.
Original languageEnglish
Place of PublicationKongens Lyngby
PublisherTechnical University of Denmark
Number of pages43
Publication statusPublished - 2013
SeriesD T U Compute. Technical Report
Number2013-01
ISSN1601-2321

Cite this

Simonsen, K. I., Kristensen, L. M., & Kindler, E. (2013). Code Generation for Protocols from CPN models Annotated with Pragmatics. Kongens Lyngby: Technical University of Denmark. D T U Compute. Technical Report, No. 2013-01
Simonsen, Kent Inge ; Kristensen, Lars Michael ; Kindler, Ekkart. / Code Generation for Protocols from CPN models Annotated with Pragmatics. Kongens Lyngby : Technical University of Denmark, 2013. 43 p. (D T U Compute. Technical Report; No. 2013-01).
@book{94b0852d494a4aa5994b61e02281b081,
title = "Code Generation for Protocols from CPN models Annotated with Pragmatics",
abstract = "Model-driven engineering (MDE) provides a foundation for automatically generating software based on models. Models allow software designs to be specified focusing on the problem domain and abstracting from the details of underlying implementation platforms. When applied in the context of formal modelling languages, MDE further has the advantage that models are amenable to model checking which allows key behavioural properties of the software design to be verified. The combination of formally verified models and automated code generation contributes to a high degree of assurance that the resulting software implementation satisfies the properties verified for the model. Coloured Petri Nets (CPNs) have been widely used to model and verify protocol software, but limited work exists on using CPN models of protocol software as a basis for automated code generation. In this report, we present an approach for generating protocol software from a restricted class of CPN models. The class of CPN models considered aims at being descriptive in that the models are intended to be helpful in understanding and conveying the operation of the protocol. At the same time, a descriptive model is close to a verifiable version of the same model and sufficiently detailed to serve as a basis for automated code generation when annotated with code generation pragmatics. Pragmatics are syntactical annotations designed to make the CPN models descriptive and to address the problem that models with enough details for generating code from them tend tobe verbose and cluttered. Our code generation approach consists of three main steps, starting from a CPN model that the modeller has annotated with a set of pragmatics that make the protocol structure and the control-flow explicit. The first step is to compute for the CPN model, a set of derived pragmaticsthat identify control-flow structures and operations, e. g., for sending and receiving packets, and for manipulating the state. In the second step, an abstract template tree (ATT) is constructed providing an association between pragmatics and code generation templates. The ATT then directs the code generation in the third step by invoking the code templates associated with each node of the ATT in order to generate code. We illustrate our approach using an example of a unidirectional data framing protocol.",
author = "Simonsen, {Kent Inge} and Kristensen, {Lars Michael} and Ekkart Kindler",
year = "2013",
language = "English",
series = "D T U Compute. Technical Report",
publisher = "Technical University of Denmark",
number = "2013-01",

}

Simonsen, KI, Kristensen, LM & Kindler, E 2013, Code Generation for Protocols from CPN models Annotated with Pragmatics. D T U Compute. Technical Report, no. 2013-01, Technical University of Denmark, Kongens Lyngby.

Code Generation for Protocols from CPN models Annotated with Pragmatics. / Simonsen, Kent Inge; Kristensen, Lars Michael; Kindler, Ekkart.

Kongens Lyngby : Technical University of Denmark, 2013. 43 p. (D T U Compute. Technical Report; No. 2013-01).

Research output: Book/ReportReportResearch

TY - RPRT

T1 - Code Generation for Protocols from CPN models Annotated with Pragmatics

AU - Simonsen, Kent Inge

AU - Kristensen, Lars Michael

AU - Kindler, Ekkart

PY - 2013

Y1 - 2013

N2 - Model-driven engineering (MDE) provides a foundation for automatically generating software based on models. Models allow software designs to be specified focusing on the problem domain and abstracting from the details of underlying implementation platforms. When applied in the context of formal modelling languages, MDE further has the advantage that models are amenable to model checking which allows key behavioural properties of the software design to be verified. The combination of formally verified models and automated code generation contributes to a high degree of assurance that the resulting software implementation satisfies the properties verified for the model. Coloured Petri Nets (CPNs) have been widely used to model and verify protocol software, but limited work exists on using CPN models of protocol software as a basis for automated code generation. In this report, we present an approach for generating protocol software from a restricted class of CPN models. The class of CPN models considered aims at being descriptive in that the models are intended to be helpful in understanding and conveying the operation of the protocol. At the same time, a descriptive model is close to a verifiable version of the same model and sufficiently detailed to serve as a basis for automated code generation when annotated with code generation pragmatics. Pragmatics are syntactical annotations designed to make the CPN models descriptive and to address the problem that models with enough details for generating code from them tend tobe verbose and cluttered. Our code generation approach consists of three main steps, starting from a CPN model that the modeller has annotated with a set of pragmatics that make the protocol structure and the control-flow explicit. The first step is to compute for the CPN model, a set of derived pragmaticsthat identify control-flow structures and operations, e. g., for sending and receiving packets, and for manipulating the state. In the second step, an abstract template tree (ATT) is constructed providing an association between pragmatics and code generation templates. The ATT then directs the code generation in the third step by invoking the code templates associated with each node of the ATT in order to generate code. We illustrate our approach using an example of a unidirectional data framing protocol.

AB - Model-driven engineering (MDE) provides a foundation for automatically generating software based on models. Models allow software designs to be specified focusing on the problem domain and abstracting from the details of underlying implementation platforms. When applied in the context of formal modelling languages, MDE further has the advantage that models are amenable to model checking which allows key behavioural properties of the software design to be verified. The combination of formally verified models and automated code generation contributes to a high degree of assurance that the resulting software implementation satisfies the properties verified for the model. Coloured Petri Nets (CPNs) have been widely used to model and verify protocol software, but limited work exists on using CPN models of protocol software as a basis for automated code generation. In this report, we present an approach for generating protocol software from a restricted class of CPN models. The class of CPN models considered aims at being descriptive in that the models are intended to be helpful in understanding and conveying the operation of the protocol. At the same time, a descriptive model is close to a verifiable version of the same model and sufficiently detailed to serve as a basis for automated code generation when annotated with code generation pragmatics. Pragmatics are syntactical annotations designed to make the CPN models descriptive and to address the problem that models with enough details for generating code from them tend tobe verbose and cluttered. Our code generation approach consists of three main steps, starting from a CPN model that the modeller has annotated with a set of pragmatics that make the protocol structure and the control-flow explicit. The first step is to compute for the CPN model, a set of derived pragmaticsthat identify control-flow structures and operations, e. g., for sending and receiving packets, and for manipulating the state. In the second step, an abstract template tree (ATT) is constructed providing an association between pragmatics and code generation templates. The ATT then directs the code generation in the third step by invoking the code templates associated with each node of the ATT in order to generate code. We illustrate our approach using an example of a unidirectional data framing protocol.

M3 - Report

T3 - D T U Compute. Technical Report

BT - Code Generation for Protocols from CPN models Annotated with Pragmatics

PB - Technical University of Denmark

CY - Kongens Lyngby

ER -

Simonsen KI, Kristensen LM, Kindler E. Code Generation for Protocols from CPN models Annotated with Pragmatics. Kongens Lyngby: Technical University of Denmark, 2013. 43 p. (D T U Compute. Technical Report; No. 2013-01).