=Paper=
{{Paper
|id=Vol-1372/paper5
|storemode=property
|title=Pragmatics Annotated Coloured Petri Nets for Protocol Software Generation and Verification
|pdfUrl=https://ceur-ws.org/Vol-1372/paper5.pdf
|volume=Vol-1372
|dblpUrl=https://dblp.org/rec/conf/apn/SimonsenKK15
}}
==Pragmatics Annotated Coloured Petri Nets for Protocol Software Generation and Verification==
https://ceur-ws.org/Vol-1372/paper5.pdf
Pragmatics Annotated Coloured Petri Nets for
Protocol Software Generation and Verification
Kent Inge Fagerland Simonsen1,2 , Lars M. Kristensen1 , and Ekkart Kindler2
1
Department of Computing, Bergen University College, Norway
2
DTU Compute, Technical University of Denmark, Denmark
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.
1 Introduction
Coloured Petri Nets (CPNs) [3] and CPN Tools have been widely used for mod-
elling and verifying protocols. Examples include application layer protocols such
as IOTP, SIP and WAP, transport layer protocols such as TCP, DCCP and
SCTP, and network layer protocols such as DYMO, AODV, and ERDP [2, 8].
Formal modelling and verification have been useful in gaining insight into the
operation of the protocols and have resulted in improved protocol specifications.
However, earlier work has not fully leveraged the investment in modelling by
also taking the step to automated code generation to obtain an implementation
of the protocol under consideration. In particular, rather limited research has
been conducted into approaches that support automatic generation of protocol
implementations from such CPN models. The earlier approaches have either re-
stricted the target platform for code generation to the Standard ML language
used by the CPN Tools simulator or have considered a specific target language
based on platform-specific additions to the CPN models.
This has motivated us to develop an approach and an accompanying tool
called PetriCode to support the automated generation of protocol software from
CPN models. Our code generation approach is designed to satisfy five main
requirements. Firstly, the approach must support platform independence, i.e., it
must enable code generation for multiple languages and platforms from the same
CPN model. Secondly, the approach must support integration of the generated
code with third-party code. In particular, it must support upwards integration,
i.e., the generated code must expose an explicit interface for service invocation,
and it must support downwards integration, i.e., the ability of the generated code
80 PNSE’15 – Petri Nets and Software Engineering
to invoke and rely on underlying libraries. Thirdly, it must support verification in
that the code generation capability should not introduce complexity problems for
verification of the CPN models. Fourthly, the generated code must be readable to
enable code review and performance enhancements. Finally, the approach must
be scalable to industrial-sized protocols.
The foundation of our approach is a slightly restricted subclass of CPNs
called Pragmatic Annotated CPNs (PA-CPNs). The restrictions make explicit
the structure of the protocol system, its principals, channels, and services. A key
feature of this class of CPNs are so-called code generation pragmatics, which are
syntactical annotations to certain elements of the PA-CPNs. These pragmatics
represent concepts from the domain of communication protocols and protocol
software, which are used to indicate the purpose of the respective modelling ele-
ment. The role of the pragmatics is to extend the CPN modelling language with
domain-specific elements and make implicit knowledge of the modeller explicit
in the CPN model such that it can be exploited for code generation.
In earlier work [16], we have introduced PA-CPNs informally, and presented
the PetriCode tool [17]. In [18], we demonstrated platform independence, inte-
grateability, and readability of the generated code. In [19], we applied the ap-
proach for automatically generating an implementation of the industrial-strength
WebSocket protocol. This included demonstrating that the generated code was
interoperable with other implementations of the WebSocket protocol.
The contribution of this paper compared to our earlier work is threefold.
Firstly, motivated by the practical relevance of the net class demonstrated in
earlier work, we give a formal definition of PA-CPNs. Secondly, we discuss the
process of developing protocol software with our approach from a methodol-
ogy perspective. Thirdly, we show that PA-CPNs are amenable to verification.
Specifically, we show how the structural restrictions of PA-CPNs allow us to add
service testers to the model of the protocol, which reduce the state space of the
model. Furthermore, the structural restrictions of PA-CPNs induce a natural
progress measure that can be exploited for verification purposes by the sweep-
line state space exploration method [4].
The rest of this paper is organised as follows: Section 2 provides the back-
ground definitions and notation of CPNs that are used throughout this paper.
Section 3 gives the formal definition of PA-CPNs accompanied by an example
outlining how PA-CPNs can be used to model a transport protocol. Section 4
discusses the modelling process of PA-CPNs from an application perspective.
Section 5 formalises the concepts of tree decomposability of control flow nets
which are central in generating code for the protocol services. Section 6 shows
how to define progress measures for the sweep-line method based on service and
service tester modules of PA-CPNs, and experimentally evaluate their effect on
the verification of the transport protocol example. Finally, in Sect. 7, we sum up
the conclusions and discuss related work. We assume that the reader is familiar
with the basic concepts of Petri nets and high-level Petri nets such as CPNs.
This paper is a condensed version of a technical report [20], which contains more
motivation and detailed explanations of examples and concepts.
L. Kristensen et al: Pragmatics Annotated CPNs 81
2 Background Definitions on Coloured Petri Nets
The definition of PA-CPNs is based on the standard definition of hierarchical
CPNs [3]. Here, we briefly rephrase the definitions of CPNs. Readers familiar
with these definitions can skip this section. In this paper, we provide the syntac-
tical definitions of CPNs only, which will be restricted when defining PA-CPNs.
Since PA-CPNs are a syntactical restriction of CPNs, we do not need change the
semantics of CPNs at all.
A hierarchical CPN consists of a finite set of CPN modules, which we dis-
cuss first. Figures 1 and 2 show some CPN modules of our example (which
will be used later). The modules of a hierarchical CPNs are related to each other
via substitution transitions (shown with a double border) which can have associ-
ated submodules, and by linking places connected to the substitution transitions
(called socket places) to places (called port places) on the associated submodules.
A CPN module consists of a set of places P and a set of transition T connected
by a set of directed arcs A connecting either a transition and a place or a place
and a transition. A CPN module additionally has a set of colour sets (types) Σ
containing the types that can be used as colour sets of places and for typing a
set of variables V which can be used in arc expressions and transition guards. In
the formal definition, the colour set of each place (by convention written below
a place) is specified by means of a colour set function that maps each place to
a colour set determining the kind of tokens that may reside on the place. Each
directed arc in a CPN module has an associated arc expression used to determine
the tokens added and removed by the occurrence of an enabled transition and
is specified by an arc expression function. The arc expression of each arc may
contain variables from the set of variables V . The arc expressions are required to
have a type such that the evaluation of an arc expression on an arc connected to a
place p results in a multi-set of tokens over the colour set of the place. Transitions
may have an associated guard expression specified by means of a guard function
G which associates a boolean expression with each transition. The initial marking
of each place is specified by means of an initialisation function I which maps
each place into a (possibly empty) multi-set over the colour set of the place.
Definition 1 formally defines a CPN module. In the definition, we use Type[v]
to denote the type of a variable v, and we use EXPR V to denote the set of
expressions with free variables contained in a set of variables V . For an expression
e containing a set of free variables V , we denote by ehbi the result of evaluating
e in a binding b that assigns a value to each variable in V . We use Type[e] for
an expression e (an arc expression, a guard, or an initial marking) to denote the
type of e. For a non-empty set S, we use SM S to denote the type corresponding
to the set of all multi-sets over S.
Definition 1. A Coloured Petri Net Module (Def. 6.1 in [3]) is a tuple
CPN M = (CP N, Tsub , Pport , P T ), such that:
1. CP N = (P, T, A, Σ, V, C, G, E, I) is a Coloured Petri Net (Def. 4.2 in [3])
where:
82 PNSE’15 – Petri Nets and Software Engineering
(a) P is a finite set of places and T is a finite set of transitions T such
that P ∩ T = ∅.
(b) A ⊆ (P × T ) ∪ (T × P ) is a set of directed arcs.
(c) Σ is a finite set of non-empty colour sets and V is a finite set of typed
variables such that Type[v] ∈ Σ for all variables v ∈ V .
(d) C : P → Σ is a colour set function that assigns a colour set to each
place.
(e) E : A → EXPR V is an arc expression function that assigns an arc
expression to each arc a such that Type[E(a)] = C(p)M S , where p is the
place connected to the arc a.
(f ) G : T → EXPR V is a guard function that assigns a guard to each
transition t such that Type[G(t)] = Bool .
(g) I : P → EXPR ∅ is an initialisation function that assigns an initiali-
sation expression to each place p such that Type[I(p)] = C(p)M S .
2. Tsub ⊆ T is a set of substitution transitions.
3. Pport ⊆ P is a set of port places.
4. P T : Pport → {IN, OUT, I/O} is a port type function that assigns a port
type to each port place.
Socket places are not defined explicitly as part of a module because they
are implicitly given via the arcs connected to the substitution transitions. For a
substitution transition t, we denote by ST (t) a mapping that maps each socket
place p into its type, i.e., ST (t)(p) = IN if p is an input socket, ST (t)(p) = OUT
if p is an output socket, and ST (t)(p) = I/O if p is an input/output socket.
The definition of a hierarchical CPN is provided below. A hierarchical CPN
consists of a set of disjoint CPN modules, a submodule function assigning a
(sub)module to each substitution transition, and a port-socket relation that as-
sociates port places in a submodule to the socket places of its upper layer module.
The set of socket places for a substitution transition t consists of the places con-
nected to the substitution transition and is denoted by Psock (t). The definition
requires that the module hierarchy (to be defined in Def. 3) is acyclic in order
to ensure that there are only a finite number of instances of each module. Fur-
thermore, port and socket places can only be associated with each other, if they
have the same colour set and the same initial marking.
Definition 2. A hierarchical Coloured Petri Net (Def. 6.2 in [3]) is a four-
tuple CP NH = (S, SM , PS , FS ) where:
1. S is a finite set of modules. Each module is a Coloured Petri Net Mod-
ule s = ((P s , T s , As , Σ s , V s , C s , Gs , E s , I s ), T s , Pport
s
, P T s ). It is required
sub
that (P ∪ T ) ∩ (P ∪ T ) = ∅ for all s1 , s2 ∈ S with s1 6= s2 .
s1 s1 s2 s2
2. SM : Tsub → S is a submodule function that assigns a submodule to
each substitution transition. It is required that the module hierarchy (see
Definition 3) is acyclic.
3. PS is a port–socket relation function that assigns a port–socket re-
SM (t)
lation PS (t) ⊆ Psock (t) × Pport to each substitution transition t. It is
L. Kristensen et al: Pragmatics Annotated CPNs 83
required that ST (t)(p) = P T (p0 ), C(p) = C(p0 ), and I(p)hi = I(p0 )hi for all
(p, p0 ) ∈ PS (t) and all t ∈ Tsub .
4. FS ⊆ 2P is a set of non-empty and disjoint fusion sets such that C(p) =
C(p0 ) and I(p)hi = I(p0 )hi for all p, p0 ∈ fs and all fs ∈ FS .
The module hierarchy of a hierarchical CPN model is a directed graph with
a node for each module and an arc leading from one module to another module
if the latter module is a submodule of one of the substitution transitions of
the former module. In the definition, Tsub denotes the union of all substitution
transitions of the hierarchical CPN, and Tsub
s
denotes all substitution transitions
in a module s.
Definition 3. The module hierarchy for a hierarchical Coloured Petri Net
CP NH = (S, SM , PS , FS ) is a directed graph MH = (NMH , AMH ), where
1. NMH = S is the set of nodes.
s1
2. AMH = {(s1 , t, s2 ) ∈ NMH × Tsub × NMH | t ∈ Tsub ∧ s2 = SM (t)} is the set
of arcs.
The roots of MH are called prime modules, and the set of all prime modules
is denoted SPM .
3 Pragmatic Annotated CPNs
PA-CPNs mandate a particular structure of the CPN models and allow the CPN
elements to be annotated with pragmatics used to direct the automated code
generation. In the CPN model, pragmatics are shown by annotations enclosed
in hh ii. Pragmatics can also have some parameters, which we discuss as they
come; but we do not formalize parameters of pragmatics in general here.
A PA-CPN is organised into three levels of modules: the protocol system
level , the principal level , and the service level – reflecting the typical structure
of protocols. In order to better understand the structure of PA-CPNs, Figs. 1 and
2 show selected modules from each level of a PA-CPN model of the protocol that
we use as a running example. The protocol consists of a sender and a receiver
principal, with services for sending and receiving data messages, and for sending
and receiving acknowledgements. The sender sends each data message, one at a
time, with a bounded number of retransmissions awaiting an acknowledgement
for each data packet. In addition to the two principals, the protocol system
contains unreliable channels for transmitting messages. The complete PA-CPN
model of the example protocol is available at [17].
We formally define PA-CPNs as a tuple consisting of a hierarchical CPN: one
protocol system module (PSM), sets of principal level modules (PLMs) and ser-
vice level modules (SLMs) and channel modules (CHMs), and a structural prag-
matics mapping (SP) that maps substitution transitions (indicated by double
borders) to pragmatics representing the annotations of substitution transitions.
84 PNSE’15 – Petri Nets and Software Engineering
()
Sender Receiver ready
<>
<> <>
UNIT
Sender Receiver
1`()
false
runAck
Sender Receiver <>
Channel Channel send BOOL receiveAck
<> <>
nextSend
Endpoint Endpoint <>
Send INT RecieveAck
Channel
<> Sender
Channel
I/O
Channel Endpoint
Fig. 1. The top-level CPN system level module (left) and principal level module for
the sender principal (right) of the protocol example.
()
messgae ready
Fusion 1 I/O
<> <>
DataList 1`() UNIT
dataList
{name= senderId,
inb = [], false
outb = []} send
<>
(0,0)
dataList
1
message startSending
<> <>
INT
DataList
dataList dataList
i n 1 true
{name=senderId,
inb = inb,
(j,c)
Sender outb = outb} limit (j,c) nextSend runAck
sendMsg loop
Channel <> n <> <>
I/O if i > j I/O I/O
{name=senderId, [data = INT BOOL
Endpoint then (i,0) LimitMap
inb = inb, List.nth(dataList, i-1)] else (i, c +1)
[(e = 0 andalso
outb = outb^^[{ (i,e,str) (c < maxResend false
data
src=senderId, orelse n > i))
dest=receiverId, orelse (e = 1
packet= DATA data}]} andalso n <= i
next andalso c <
<> maxResend)]
n
Data
(i,e,str) (j,c)
ep return true
<>
[(e = 1 andalso n > i )orelse
(i <= j andalso c >= maxResend
andalso i >= n) 1`()
andalso #inb ep = [] ]
end
Fusion 4
<>
UNIT
Fig. 2. The send service level module of the protocol example.
Definition 4. A Pragmatics Annotated Coloured Petri Net (PA-CPN)
is a tuple CPN P A = (CPN H , PSM , PLM , SLM , CHM , SP ), where:
1. CPN H = (S, SM, P S, F S) is a hierarchical CPN with PSM ∈ S being a
protocol system module (Def. 5) and the only prime module of CPN H .
2. PLM ⊆ S is a set of principal level modules (Def. 6); SLM ⊆ S is a
set of service level modules (Def. 7) and CHM ⊆ S is a set of channel
modules s.t {{PSM }, PLM , SLM , CHM } constitute a partitioning of S.
3. SP : Tsub → {principal, service, internal, channel} is a struc-
tural pragmatics mapping such that:
(a) Substitution transitions with hhprincipalii have an associated principal
level module: ∀t ∈ Tsub : SP (t) = principal ⇒ SM (t) ∈ PLM .
(b) Substitution transitions with hhserviceii or hhinternalii are associated with
a service level module:
∀t ∈ Tsub : SP (t) ∈ {service, internal} ⇒ SM (t) ∈ SLM .
L. Kristensen et al: Pragmatics Annotated CPNs 85
(c) Substitution transitions with hhchannelii are associated with a channel
module: ∀t ∈ Tsub : SP (t) = channel ⇒ SM (t) ∈ CHM .
It should be noted that channel modules do not play a role in the code
generation; they constitute a CPN model artifact used to connect the principals
for verification purposes. Therefore, we do not impose any specific requirements
on the internal structure of channel modules.
Protocol system level. The module shown in Fig. 1(left) comprises the pro-
tocol system level of the PA-CPN model of the example. It specifies the two
protocol principals in the system and the channel connecting them. The sub-
stitution transitions representing principals are specified using the principal
pragmatic, and the substitution transitions representing channels are specified
using the channel pragmatic. The PSM module is defined as a tuple consisting
of a CPN module and a pragmatic mapping P M that associates a pragmatic
to each substitution transition. The requirement on a protocol system module
is that all substitution transitions must be substitution transitions that are an-
notated with either a principal or a channel pragmatic. Furthermore, two
substitution transitions representing principals cannot be directly connected via
a place: there must be a substitution transition representing a channel in be-
tween. This reflects the fact that principals can communicate via channels only.
Definition 5. A Protocol System Module of a PA-CPN with a structural
pragmatics mapping SP is a tuple CPN PSM = (CPN PSM , PM ), where:
1. CPN PSM = ((P PSM , T PSM , APSM , Σ PSM , V PSM , C PSM , GPSM , E PSM , I PSM ),
PSM
Tsub PSM
, Pport , PT PSM ) is a CPN module such that all transitions are substi-
tution transitions: T P SM = Tsub
P SM
.
2. PM : Tsub → {principal, channel} is a pragmatics mapping s.t.:
PSM
(a) All substitution transitions are annotated with either a principal or
channel pragmatic: ∀t ∈ Tsub PSM
: PM (t) ∈ {principal, channel}.
(b) The pragmatics mapping PM must coincide with the structural pragmatic
mapping SP of PA-CPN: ∀t ∈ Tsub PSM
: PM (t) = SP (t).
(c) All places are connected to at most one substitution transition with hhprincipalii
and at most one substitution transition with hhchannelii:
∀p ∈ P PSM : ∀t1 , t2 ∈ X(p) : PM (t1 ) = PM (t2 ) ⇒ t1 = t2 .
Principal level. On the principal level, there is one module for each principal
of the protocol as defined by hhprincipalii on the protocol system level. The exam-
ple protocol has two modules at the principal level corresponding to the sender
and the receiver. Figure 1(right) shows the principal level module for the sender.
A principal level module is required to model the services that the principal is
providing, and the internal states and life-cycle of the principal. For the sender,
there are two services as indicated by the service and internal pragmatics
on the substitution transitions send (for sending messages) and receiveAck (for
86 PNSE’15 – Petri Nets and Software Engineering
receiving acknowledgements). Services that can be externally invoked are speci-
fied using the service pragmatic, whereas services that are to be invoked only
internally are specified using the internal pragmatic. The non-port places of
a principal level module (places drawn without a double border) can be anno-
tated with either a state or an LCV pragmatic. Places annotated with a state
pragmatic represent internal states of the principal. In Fig. 1(right), there are
two places with hhstateii used to enforce a stop-and-wait pattern in sending data
messages and receiving acknowledgements. Places annotated with an LCV prag-
matic represent the life-cycle of the principal by putting restrictions on the order
in which services can be invoked. As an example, the place ready in Fig. 1(right)
ensures that only one message at a time is sent using the send service.
Definition 6. A Principal Level Module of a PA-CPN is a tuple CPN PLM =
PLM
(CPN PLM , Tsub PLM
, Pport , PT PLM , PLP ) where:
1. CPN PLM = ((P P LM , T P LM , AP LM , Σ P LM , V P LM , C P LM , GP LM , E P LM ,
I P LM ), Tsub
PLM PLM
, Pport , PT PLM ) is a CPN module with only substitution tran-
sitions: T P LM
= Tsub .
P LM
2. P LP : TsubPLM
∪ P P LM \ Pport
P LM
→ {service, internal, state, LCV} is a
principal level pragmatics mapping satisfying:
(a) All non-port places are annotated with either a state or a LCV prag-
matic: ∀p ∈ P P LM \ PportP LM
⇒ PLP (p) ∈ {state, LCV}
(b) All substitution transitions are annotated with a service or internal
pragmatic: ∀t ∈ Tsub PSM
: PLP (t) ∈ {service, internal}.
Service level. The service level modules specify the detailed behaviour of the
individual services and constitute the lowest level modules in a PA-CPN model.
In particular, there are no substitution transitions in modules at this level. The
module in Fig. 2 is an example of a module at the service level. It models the
behaviour of the send service in a control-flow oriented manner. The control-flow
path, which defines the control flow of the service, is made explicit via the use of
the Id pragmatics. The entry point of the service is indicated by annotating a
single transition with hhserviceii, and the exit (termination) point of the service
is indicated by annotating a single transition with hhreturnii. In addition, non-
port places can be annotated with a state pragmatic to indicate that this
place models a local state of the service. The driver pragmatic is used by
service tester modules (Sect. 6) to facilitate verification. The places with hhIdii
determine a subnet of the module, which we call the underlying control-flow net:
it is obtained by removing all CPN inscriptions and considering only places with
hhIdii and transitions connected to these places, which in Fig. 2, are indicated by
places, transitions, and arcs with thick border. This control-flow net must follow
a certain structure so that there is a one-to-one correspondence to control-flow
constructs of typical programming languages. This requirement is called tree
decomposability and is formally defined in Sect. 5.
A service level module is defined as consisting of a CPN module without
substitution transitions and with service level pragmatics as described above.
L. Kristensen et al: Pragmatics Annotated CPNs 87
Note that we use the symbol ∃! to indicate that there “exists exactly on element”
with the respective property.
Definition 7. A Service Level Module of a PA-CPN is a tuple CPN SLM =
SLM
(CPN SLM , Tsub SLM
, Pport , PT SLM , SLP ) where:
1. CPN SLM = ((P SLM , T SLM , ASLM , Σ SLM , V SLM , C SLM , GSLM , E SLM ,
I SLM ), Tsub
SLM SLM
, Pport , PT SLM ) is a CPN module without substitution transi-
tions: Tsub = ∅.
SLM
2. SLP : T SLM ∪ P SLM \ Pport SLM
→ {Id, state, service, return, driver}
is a service level pragmatic mapping satisfying:
(a) Each place is either annotated with Id, state, driver or is a port
place : ∀p ∈ P SLM \ Pport
SLM
: SLP (p) ∈ {Id, state, driver}.
(b) There exits exactly one transition with hhserviceii and exactly one tran-
sition with hhreturnii:
∃!t ∈ T SLM : SLP (t) = service and ∃!t ∈ T SLM : SLP (t) = return.
3. For all t ∈ T SLM and p ∈ P SLM we have:
(a) Transitions consume one token from input places with an Id pragmatic:
(p, t) ∈ ASLM ∧ SLP (p) = Id ⇒ |E(p, t)hbi| = 1 for all bindings b of t.
(b) Transitions produce one token on output places with an Id pragmatic:
(t, p) ∈ ASLM ∧ SLP (p) = Id ⇒ |E(t, p)hbi| = 1 for all bindings b of t.
(c) Only transitions with hhserviceii can have input places with hhdriverii:
(p, t) ∈ ASLM ∧ SLP (p) = driver ⇒ SLP (t) = service
(d) Only transitions with hhreturnii can have output places with hhdriverii
pragmatic: (t, p) ∈ ASLM ∧ SLP (p) = driver ⇒ SLP (t) = return
4. The underlying control flow net of CPN SLM is tree decomposable (Defs. 9,11).
4 Protocol Modelling Process
In the previous sections, we have formalised the structural restrictions of CPNs
and the pragmatics extensions that make them Pragmatic Annotated CPNs (PA-
CPNs); some additional restrictions on the control-flow structure and the service
testers will be formalized later in Sect. 5 and 6. Since it is the modellers respon-
sibility to come up with a model meeting these requirements, we briefly discuss
the choices underlying the definition of PACPNs and their structural restrictions
concerning the modelling process and some methodology for developing protocol
software with PA-CPNs here.
The structural requirements of PA-CPNs have been distilled from the expe-
rience with earlier CPN models of protocols. The structure and annotations of
PA-CPNs are designed to help the modeller come up with a clear model and to
give clear guidelines for creating a model that – at the same time – can be used
for code generation as well as for verification. As such, the structure of PA-CPNs
should be driven by the protocol and its purpose rather than by the artifacts
of Petri nets. This is, in particular, reflected by structuring the model in three
layers: protocol system, principal, and service layer.
88 PNSE’15 – Petri Nets and Software Engineering
The top layer, the protocol system layer, identifies the overall structure of
the protocol, which are the principals of the protocol and how the principals are
connected by channels (see Fig. 1 (left) for an example). Each principal and each
channel is represented by a substitution transition with a respective annotation,
and places connecting the respective principals with channels. The behaviour
of each principal is represented by principal level module, which identifies the
services of the respective principal (see Fig. 1 (right) for an example) along with
the states of the protocol and its life-cycle. The services are represented by sub-
stitution transitions annotated with the service pragmatics, the state and the
life-cycle of the principal are represented by places with state and LCV prag-
matics. The behaviour of each service is then modelled by a service level module,
which is associated with the service substitution transitions on the principal
level module (see Fig. 2 for an example). The service level module has access
to the channels that the principal is connected to as well as to the principal’s
state and life-cycle variables. The most prominent structure (indicated by bold-
faced places, transitions, and arcs) of the service level module is the control-flow
structure, which is identified by the Id pragmatics and which needs to follow
very specific rules so that it can be transformed to control-flow constructs of
typical programming languages and result in human-readable code. The exact
requirements are discussed in Sect. 5.
It should be noted that also the channels (on the protocol system level)
need to be associated with PA-CPN modules, which model the exact behaviour
of the respective channel. The modules for the channels are not used for code
generation, since the generated code will use implementations of channels from
the underlying platform (based on the properties required for these channels).
But for verifying the protocol with standard CPN mechanisms, we need a CPN
module for each channel, which however does not have any further structural
restrictions.
Any model that meets the requirements of PA-CPNs can be used for code
generation as well as for verification – irrespective of the way it was produced.
The typical modelling process of protocols with PA-CPN starts at the top-level
by identifying the principals of the protocol and how they are connected by
channels. Then, the services of each principal are identified on the principal
level, and then each service is modelled. So the general modelling direction is
top-down. Of course, additional services and even additional principals could be
added later, when need should be.
5 Tree Decomposability of Control Flow Nets
As discussed earlier, the control-flow structure of a service level module, called
the underlying control-flow net, must correspond one-to-one to control-flow con-
structs of programming languages. The main purpose of this requirement is to
generate readable code. In this section, we formally define the underlying control
flow net of a service level module and its one-to-one correspondence to control-
flow constructs. This is achieved by inductively decomposing the control-flow net
L. Kristensen et al: Pragmatics Annotated CPNs 89
into a tree of sub-blocks, each of which corresponds to a control-flow construct:
atomic step, sequence, choice and loop.
Figure 3 shows the underlying control flow net of the service level module
from Fig. 2. All places and transitions in the rounded rectangle (representing the
block border) are part of the block; an arrow from the block border to a place
indicates the entry place; an arrow from a place to the block border indicates
the exit place. The control flow net in Fig. 3 can be decomposed in a loop block,
which in turn consists of an atomic block.
First, we define blocks: these are Petri nets with a fixed entry and exit place.
Definition 8. Let N = (P, T, A) be a Petri net and s, e ∈ P . Then B =
(P, T, A, s, e) is called a block with entry s and exit e. The block is atomic, if
P = {s, e}, s 6= e, |T | = 1 and for t ∈ T , we have • t = {s} and t• = {e}. The
block has a safe entry, if s 6= e and • s = ∅. The block has a safe exit, if s 6= e
and e• = ∅.
For easing the following definitions, we in-
troduce an additional notation: For a block
Bi , we refer to its constituents by Bi =
(Pi , Ti , Ai , si , ei ) without explicitly naming
them every time. The block that is under-
lying a service level module is determined by
all the places with hhIdii pragmatics and the
transitions in their pre- and postsets. The
unique transition with hhserviceii defines the
entry place, and the unique transition with
hhreturnii defines the exit place of this block;
note that for technical reasons, these two
transitions are not part of the block. There-
Fig. 3. Decomposition of the ser-
fore, these transitions are shown by dashed
vice level module in Fig. 2
lines in Fig. 3. Formally, the control flow net
underlying a service level module is defined as follows.
Definition 9. Let CPN SLM be a service level module as defined in Def. 7. Let
P = {p ∈ P SLM \ Pport SLM
|SLP (p) = Id}, let T = T SLM ∩ • P ∩ P • , and let
A = ASLM ∩ ((T × P ) ∪ (P × T ))}; moreover, let s ∈ P be the unique place
such that there exists a transition t ∈ T = T SLM with (t, s) ∈ ASLM and
SLP (t) = service, and let e ∈ P be the unique place e such that there exists
a transition t ∈ T = T SLM with (e, t) ∈ ASLM and SLP (t) = return. Then,
N = (P, T, A, s, e) is the underlying control flow net of CPN SLM .
The control flow of the code that is being generated is obtained by decom-
posing the underlying control flow net of a service level module into sub-blocks
representing the control-flow constructs. We define the decomposition in a very
general way at first, which does not yet restrict the possible control-flow con-
structs. The decomposition into blocks, just makes sure that all parts of the
block are covered by sub-blocks and that they overlap on entry and exit places
90 PNSE’15 – Petri Nets and Software Engineering
only. In a second step, the decomposition is restricted in such a way that the
decomposition captures certain control flow constructs (Def. 11).
Definition 10. Let B = (N, s, e) be a block with net N = (P, T, F ). A set of
blocks B1 , . . . , Bn is a decomposition of B if the following conditions hold:
1. The sub-blocks contain only elements from B, i. e. for each i ∈ {1, . . . , n},
we have Pi ⊆ P , Ti ⊆ T , and Fi ⊆ F ∩ ((Pi × Ti ) ∪ (T Sin× Pi )). Sn
2. The sub-blocks
Sn contain all elements of B, i. e. P = i=1 Pi , T = i=1 Ti ,
and F = i=1 Fi .
3. The inner structure of all sub-blocks are disjoint, i. e. for each i, j ∈ {1, . . . , n}
with i 6= j, we have Ti ∩ Tj = ∅ and Pi ∩ Pj = {si , ei } ∩ {sj , ej }.
As the final step, we define when a decomposition of a block reflects some
control flow construct. The definition does not only define decomposability into
control flow constructs; it also defines a tree structure which reflects the control-
flow structure of the block; the type of each node reflects the construct. The
definition is illustrated in Fig. 4. The top left part of Fig. 4 shows the inductive
definition of a loop construct: The assumptions are that two blocks B1 and B2
are identified already. B1 is any kind of block (represented by X) with a safe
entry place s and a safe exit place e; B2 is an atomic block with entry place e
and exit place s. Thus, block B1 represents the loop body, and block B2 the
iteration. Then, the union of both blocks and entry place s and exit place e,
form a block B, which is a loop consisting of the loop body B1 and the atomic
block B2 for the iteration. The definitions of choices and sequences are similar.
Fig. 4. Inductive definition of block trees
Definition 11 below formally defines block tree as illustrated in Fig. 4.
Definition 11. The block trees associated with a block are inductively defined:
L. Kristensen et al: Pragmatics Annotated CPNs 91
Atomic If B is an atomic block, then the tree with the single node B:atomic
is a block tree associated with B.
Loop If B is a block and B1 and B2 is a decomposition of B, and for some X,
B1 : X is a block tree associated with B1 , and B2 : atomic is a block tree
associated with B2 , and if B1 has a safe entry and a safe exit s.t s1 = s,
e1 = e, s2 = e, e2 = s, then the tree with top node B:loop and the sequence
of sub-trees B1 : X and B2 : atomic is a block tree associated with B.
Choice If B is a block and for some n with n ≥ 2 the set of blocks B1 , . . . , Bn
is a decomposition of B, and have a safe entry and a safe exit, and B1 :
X1 , . . . , Bn : Xn for some X1 , . . . , Xn are block trees associated with B1 , . . . , Bn ,
and if for all i ∈ {1, . . . , n}: si = s and ei = e, then the tree with top node
B:choice with the sequence of sub-trees Bi : Xi is a block tree associated
with B.
Sequence If B is a block and for some n with n ≥ 2 the set of blocks B1 , . . . , Bn
is a decomposition of B, and, for some X1 , . . . , Xn , the trees B1 : X1 , . . . , Bn :
Xn are block trees associated with B1 , . . . , Bn , and if there exist different
places p0 , . . . , pn ∈ P such that s = p0 , e = pn , and for each i ∈ {0, . . . , n−1}
we have si = pi , ei = pi+1 , and Bi has a safe exist or Bi+1 has a safe entry,
then the tree with top node B:sequence and the sequence of sub-trees Bi : Xi
is a block tree associated with B.
A net for which such a tree exists is said to be tree decomposable.
Note that in order to simplify the definition of tree decomposability, the tree
decomposition of a block is not necessarily unique according to our definition.
For example, a longer sequence of atomic blocks could be decomposed in different
ways. In the PetriCode tool, such ambiguities are resolved by making sequences
as large as possible. Note also that for two consecutive constructs in a sequence,
it should not be possible to go back from the second to the first; therefore, the
above definition requires that consecutive blocks have a safe entry or a safe exit.
And there are some similar requirements for loops and choices.
6 Service Testers and Sweep-Line Verification
The service level modules constitute the active part of a PA-CPN model. The
execution of an individual service provided by a principal starts at the transition
with a hhserviceii pragmatic. The transitions annotated with a service pragmatic
typically has a number of parameters which need to be bound to values in order
for the transition to occur. An example of this is the Send service transition in
Fig. 2 which has the variable dataList as a parameter. This means that there are
often an infinite number of bindings for a service transition.
To control the execution of a PA-CPN model in verification by means of state
space exploration, we introduce the concept of service tester modules which can
be used to guide the verification process and represent a user of the services
provided by the principal modules. An advantage of service testers is that they
92 PNSE’15 – Petri Nets and Software Engineering
contribute to reducing the state space during verification and enable progress
measures for the sweep-line method [4] to be automatically computed.
The service tester modules are connected to the rest of the PA-CPN model
through fusion sets, and the service tester modules invoke the service provided
by the principal by putting tokens on fusion places and the service tester receives
any results from the invoked services via tokens on these places.
Fusion sets and fusion places are standard
constructs of hierarchical CPNs (see Def. 2). A
()
d0
<>
fusion set consists of a set of fusion places such () 1`(1, 0, "Col")++
1`(2, 0, "our")++
that removing (adding) tokens from (to) a fusion
Fusion 1
1`(3,1,"ed ") message
Call send
<>
place is reflected on the markings of all members ()
DataList
of the fusion set. In addition to the fusion places, d1
<>
Id pragmatics are used to make the control flow ()
()
Fusion 2
of the service tester explicit in a similar manner
call Receive
call receive
<>
as for service level modules. ()
Figure 5 shows an example of a service tester
d2
<>
Fusion 3
module for the PA-CPN model introduced in () endReceive
() <>
Sect. 3. The service tester drives the execution cleanReceiver () Fusion 4
sendFinished
of a CPN model through fusion places. A ser- () <>
vice tester module can have many places with Id
d3
<>
pragmatics; but only one of them may contain a
token initially (place d0 in Fig. 5). The service Fig. 5. Service tester module
tester first invokes the send service in Fig. 2 by
putting a token in the fusion place message. Next, the service tester invokes the
receive service in the receiver principal. Service tester modules are formalised
below.
Definition 12. A Service Tester Module is a tuple CPN STM = (CPN STM ,
STM
Tsub STM
, Pport , PT STM , TPM ) where:
1. CPN STM = ((P ST M , T ST M , AST M , Σ ST M , V ST M , C ST M , GST M , E ST M ,
I ST M ), Tsub
STM STM
, Pport , PT STM ) is a CPN module with no substitution tran-
sitions: Tsub = ∅.
STM
2. TPM : P ST M → {Id, driver, LCV} is a tester pragmatic mapping.
3. ∃!p ∈ I: |I ST M (p)hi| = 1, and for all t ∈ T ST M and p ∈ P ST M we have:
(a) Transitions consume one token from input places with an Id pragmatic:
(p, t) ∈ AST M ∧ T P M (p) = Id ⇒ |E(p, t)hbi| = 1 for all bindings b of t.
(b) Transitions produce one token on output places with an Id pragmatic:
(t, p) ∈ AST M ∧ T P M (p) = Id ⇒ |E(t, p)hbi| = 1 for all bindings b of t.
4. Transitions and places with an LCV pragmatic must be connected with a
double arc: ∀p ∈ P ST M , t ∈ T ST M : T P M (p) = LCV ⇒ ((t, p) ∈ AST M ⇔
(p, t) ∈ AST M )
5. The underlying control flow block of CPN STM is tree decomposable (Defs. 9,11).
Service tester modules are connected to a PA-CPN by means of fusion places
in order to control the execution of the services. We therefore define a PA-CPN
L. Kristensen et al: Pragmatics Annotated CPNs 93
equipped with service tester modules as a hierarchical CPN consisting of a set
of modules that constitute a PA-CPN according to Def. 4 and a set of service
tester modules which are all prime modules. We also require that fusion places
are connecting the service level modules and the service tester module so that
they correspond to the invocation of services and collecting of a results from
an executed service. As with PA-CPNs, the modeller must construct the service
tester modules such that they satisfy the formal requirements. Due to space
limitations we omit the formal definition of PA-CPNs with service testers which
can be found as Def. 5.2 in [20].
The set of service tester modules determine the state space of the PA-CPN
model under analysis. The service tester modules may specify a more or less strict
execution order on the services being invoked. It is therefore possible to use the
service tester modules to control the size of the state space of the PA-CPN model
being verified. Below we show that in addition to the use of service testers, the
structural requirements imposed by PA-CPNs can be exploited by the sweep-line
method [4] to further reduce the peak memory usage during verification.
The sweep-line method addresses the state explosion problem by exploiting a
notion of progress exhibited by many systems to store subsets of the state space
in memory during state space exploration. To apply the sweep-line method, a
progress measure must be provided for the model as formalised below where
S denotes the set of all states (markings), →∗ the reachability relation on the
markings of the CPN model, and R(M0 ) denotes the states reachable from the
initial marking M0 .
Definition 13. A progress measure is a tuple P = (O, v, ψ) such that O is a
set of progress values, v is a total order on O, and ψ : S → O is a progress
mapping. P is monotonic if ∀s, s0 ∈ R(M0 ) : s →∗ s0 ⇒ ψ(s) v ψ(s0 ).
Otherwise, P is non-monotonic.
The subsets of states that need to be stored at the same time are determined
via a progress value assigned to each state, and the method explores the states in
a least-progress-first order. The sweep-line method explores states with a given
progress value before progressing to the states with a higher progress value.
When the method proceeds to consider states with a higher progress value, it
deletes the states with a lower progress value from memory. If it turns out that
the system regresses (a non-monotonic progress measure), then the method will
mark states at the end of regress edges as persistent (i. e., store them permanently
in memory) in order to ensure termination. In the presence of regression, the
sweep-line method may visit the same state multiple times (for details, see [4]).
The structure imposed on CPNs by PA-CPNs and services testers means that
PA-CPN models have several potential sources of progress. The control-flow in
the service modules is one source of progress as there is a natural progression
from the entry point of the service towards the exit point of the service. The
life-cycle of a principal is another potential source of progress as there will often
be an overall intended order in which the services provided are to be invoked,
94 PNSE’15 – Petri Nets and Software Engineering
and this will be reflected in the life-cycle variables of the principal. Finally, the
service testers are also a source of progress as a service tester will inherently
progress from the start of the test towards the end of the test. For our example
protocol, the progress mapping can be defined as a vector of place-wise measures
using the number of tokens on some of its places. This is written below where
we omitted the parts of the model that we did not show in this paper and used
s(p) to denote the marking of a place p in the state s:
ψ(s) = (|s(d0)|, |s(d1)|, |s(d2))|, |s(d3)|, |s(startSnd)| + |s(next)|, |s(end)|) (1)
Two such vectors can be compared lexicographically, meaning the order of
the different entries represents their significance. The first four entries represent
the progress in the service tester (Fig. 5). The next two entries represent the
progress within the send service (Fig.2). Note that since the places startSending
(abbreviated as startSnd in (1) and (2)) and next are on a loop, tokens can
flow back from place next to place startSending. The end place is actually the
respective driver place from the tester, which propagates the progress between
the service and tester. Therefore, the tokens on both places within this loop are
counted the same (added up in the same entry of the vector). An alternative
progress measure is shown below (omitting the parts of the model that we did
not show in this paper):
ψ(s) = (|s(d0)|, |s(d1)|, |s(d2))|, |s(d3)|, |s(startSnd)|, |s(next)|, |s(end)|) (2)
The difference between (1) and (2) is how loops are handled. In the progress
measure (2), the places on loops are appended to the vector as if the loop was not
there. In the present example this is shown by having replaced the + operator
in (1) between startSending and next with a comma in (2).
We generalise the above idea by defining progress measures on top of the tree
decomposition of the blocks underlying the corresponding service tester module
or the service level module. We define a simple progress measure and a complex
one. The simple one is monotonic and adds up the number of all tokens within
a top-level loop; the complex one is not monotonic, but takes progress within
a loop into account. Since both definitions are very similar, we define only the
complex progress measures formally here (the simple one can be found in [20]).
Definition 14. Let BT be a block tree for a CP N module. The sequence of
complex progress measure entries is defined inductively over the block tree
BT of the CP N module:
Atomic If BT is B : atomic, then complex progress sequence consist of |s|, |e|
where s is the entry place of the block B and e is the exit place.
Sequence If BT is B : sequence with subblocks B1 , . . . Bn , and e1i , . . . , eki i are
the complex progress sequences for Bi , then e11 , . . . , e1k1 −1 , e12 , . . . , ek22 −1 , . . . ,
e1n , . . . , eknn is the complex sequence for BT .
Choice If BT is B : choice with subblocks B1 , . . . Bn , and e1i , . . . , ek1i are the
complex progress sequence for each block Bi , then the sequence e11 , . . . , e1k1 −1 ,
e22 , . . . , ek22 −1 , . . . , e2n , . . . , eknn is the complex progress sequence for BT
L. Kristensen et al: Pragmatics Annotated CPNs 95
Loop If BT is B : loop with places with sub-block B1 and B2 with the complex
progress sequence e1 , . . . , en for B1 , then e1 , . . . , en is the complex progress
sequence for BT .
A progress measure for the complete system can be built from the progress
sequences (either the simple or the complex one) for the tester and service mod-
ules by concatenating the sequences. The concatenation would first choose the
sequences for the service testers and then the sequences for all the service level
modules. Note that if there is a driver place of a service tester attached to the
service, this driver place would also be added to the progress measure sequence
of the service level module at the end (as for the end place for the send service).
Table 1 shows some experimental performance results on the protocol exam-
ple for different configurations (number of transmitted messages) and channel
characteristics (lossy/non-lossy) using the sweep-line method with the simple
and the complex progress measure. In the experiments, we consider exploration
of the complete state space. This is done since the sweep-line method (unless
combined with other reduction techniques) in the worst-case needs to explore
all states in order to model check a property. One example of this is checking
that in all terminal states, the protocol has correctly delivered all packets. Since
the simple progress measure is monotonic, the number of explored states using
that measure is identical to the number reachable states of the respective exam-
ple, which for clarity are indicated in the first column again. Since the complex
progress measure is not monotonic, some states might be visited (explored) mul-
tiple times. Therefore, the number of explored states is higher than the reachable
states of the respective example. The ratio columns give the ratio in percent be-
tween the peak number of states stored (with the respective progress measure)
and the number of reachable states. It can be seen that the runtime as well
the peak memory use are better when using the complex progress measure. The
complex measure provides better performance due to the fact that the send ser-
vice has a loop as the top-level control-flow construct. It can be seen that the
peak memory use with the complex progress measure is reduced to between 40
and 77%.
Table 1. Verification using simple and complex progress measure
Config Simple PM Complex PM
Reachable Explored Peak Ratio Time Explored Peak Ratio Time
1:noloss 156 156 77 49.3 <1 s 165 63 40.3 <1 s
1:lossy 186 186 99 53.2 <1 s 196 78 41.9 <1 s
3:noloss 2,222 2,222 2,014 90.6 <1 s 2790 1,582 71.2 <1 s
3:lossy 2,928 2,928 2,700 92.2 <1 s 4037 2,187 75.7 <1 s
7:noloss 117,584 117,584 115,373 98.1 216 s 143,531 86,636 73.6 32 s
7:lossy 160,620 160,620 158,888 98.1 532 s 263,608 124,661 77.6 80 s
96 PNSE’15 – Petri Nets and Software Engineering
7 Conclusions and Related Work
In this paper, we focused on the formal definition of PA-CPNs and how the struc-
ture of PA-CPNs can be exploited for more efficient verification. The PA-CPN
net class has been motivated by the objective of developing a code generation
approach to protocol software which allows the same model to be used for both
code generation and verification – and which satisfies five main requirements:
platform independence, code integration, verifiability, readability, and scalability.
The development of PA-CPNs has been driven by practical experiments in order
to empirically validate that the approach satisfied the five requirement in prac-
tice. The experimental results have been reported in earlier papers [16, 17, 19]
using an implementation of the approach in the PetriCode tool.
The requirements of platform independence, code integration, readability, and
scalability are relevant for use in practice: Platform independence ensures that
the approach is not locked to a particular target programming language. Code
integration ensures that the generated code can be integrated with existing other
parts of the software. Readability of the generated code is important for devel-
oping trust in the approach, and for further maintaining the protocol software
in the future. Scalability is important for being able to apply the approach to
industrial strength protocols. Concerning verifiability, it often is the case that
one model is used for verification, and then the protocol is implemented manu-
ally from that or generated from another model. This imposes extra work and
decreases the confidence in that the actual software meets the requirements ver-
ified on the model. Therefore, we required the same model being used for code
generation and for verification.
As stated in the introduction, CPNs have been primarily used for modelling
and verifying protocols in the past. Still, related approaches for CPNs – and
more generally for high-level Petri Nets (HLPNs) – have been developed. Below,
we relate our work to other approaches using HPLNs for code generation by
discussing them in the context of the five requirements that have driven the
development of PA-CPNs.
Kaim [6] contains a generic discussion of aspects related to generating code
from low-level and high-level Petri net models with the purpose of executing
it outside the simulation environment where they are created. Kaim discusses
both centralised and parallel approaches to interpretation of Petri net models.
A main aspect of the parallel approach is a structural analysis of the model
in order to identify subnets that can be mapped to different processes. In the
PetriCode approach, the structural pragmatics provided by the modeller and the
structural restrictions of PA-CPNs provide similar information. Kaim does not
consider the issues of code integration and the readability of the generated code.
The approach presented by Philippi [14] is a hybrid of simulation-based and
structural analysis approaches to code generation for HLPNs. The motivation
for the hybrid approach is to produce more readable code than a pure simulation
approach would because fewer checks are needed in the code. Philippi targets
the Java platform only and is therefore not platform independent in its basic
form. The generated code can be integrated into third party code in that the
L. Kristensen et al: Pragmatics Annotated CPNs 97
API of the generated code is defined by UML class diagrams. The paper [14]
does not discuss the scaling to large applications. Lassen et al. [11] aim to gen-
erate readable code by creating code with constructs that are similar to what
human programmers would have created. Since the approach of Lassen is based
on Java annotations of CPN models, the approach is tailored to the Java pro-
gramming language and does not provide a generic infrastructure that supports
code generation for different platforms.
Reinke [15] studies, in the context of the functional programming language
Haskell, how to use language embedding for mapping constructs from HLPNs
into Haskell code. The focus of Reinke is on generating code for a HLPN sim-
ulator. The work of Reinke is not aimed at providing a general mechanism for
generating readable code and on integrating the code into a larger application.
Kummer et al. [10] are concerned with the execution of reference nets in the
context of the Renew tool which is based on the Java platform. Reference nets
as supported by Renew are known to be verifiable [12] but the approach is specif-
ically tailored to the Java platform. The work does not focus on integration at
the code level but other means are providing for integrating the code into larger
applications [1].
Mortensen’s approach [13] is a simulation based approach based on extracting
the generated simulation code from CPN Tools. As such the work of Mortensen
is aimed at making an SML implementation of the modelled system and not
on conducting verification of the models or to target multiple platforms. Fur-
thermore, being a simulation based approach, the goal from the outset is not to
generate code that is intended for humans to read. The use of a simulation-based
approach also means that there is a considerable performance overhead due to
the many enabling checks in the code. The approach of Kristensen et al. [7] is
similar to the approach in [13]. PP-CPNs are used in [9] as the basis for code
generation targeting the Erlang language but the approach is not designed to
address readability of the generated code. Furthermore, the approach is tailored
to the Erlang platform and may not be easily adapted to other platforms even
though PP-CPNs and the intermediary representation of control-flow graphs are
independent of the target language. Jørgensen et al. [5] propose an approach for
generating BPEL code. The approach is targeted at BPEL and does not cre-
ate code for other languages or aims to address verifyability, code integration,
readability and scalability.
It follows from the discussion above that PA-CPNs and the PetriCode ap-
proach complement existing related approaches to code generation for high-level
Petri Nets. Furthermore, none of the approach discussed above specifically ad-
dress the domain of protocol software. This paper can be viewed as completing
the development of the PA-CPN net class by giving a formal definition and hence
establishing the formal foundation of our approach.
References
1. T. Betz et al. Integrating web services in Petri net-based agent applications. In
Proc. of PNSE’13, pages 97–116, 2013.
98 PNSE’15 – Petri Nets and Software Engineering
2. J. Billington, G.E. Gallasch, and B. Han. A Coloured Petri Net Approach to
Protocol Verification. In Lectures on Concurrency and Petri Nets, volume 3098 of
LNCS, pages 210–290. Springer, 2004.
3. K. Jensen and L.M. Kristensen. Coloured Petri Nets - Modelling and Validation
of Concurrent Systems. Springer, 2009.
4. K. Jensen, L.M. Kristensen, and T. Mailund. The Sweep-line State Space Explo-
ration Method. Theoretical Computer Science, 429:169–179, 2012.
5. J. B. Jørgensen and K. B. Lassen. Let’s Go All the Way: From Requirements via
Colored Workflow Nets to a BPEL Implementation of a New Bank System. In In
Proc. of CoopIS’05, volume 3760 of LNCS, pages 22–39. Springer, 2005.
6. W. El Kaim and F. Kordon. Code generation. In C. Girault and R. Valk, editors,
Petri Nets for System Engineering, chapter 21, pages 433–470. Springer, 2003.
7. L. M. Kristensen, P. Mechlenborg, L. Zhang, B. Mitchell, and G. E. Gallasch.
Model-based Development of a Course of Action Scheduling Tool. International
Journal on Software Tools for Technology Transfer, 10:5–14, 2008.
8. L.M. Kristensen and K.I.F. Simonsen. Applications of Coloured Petri Nets for
Functional Validation of Protocol Designs. In ToPNoc VII, volume 7480 of LNCS,
pages 56–115. Springer, 2013.
9. L.M. Kristensen and M. Westergaard. Automatic Structure-Based Code Genera-
tion from Coloured Petri Nets: A Proof of Concept. In Proc. of FMICS’10, volume
6371 of LNCS, pages 215–230. Springer, 2010.
10. O. Kummer et al. An Extensible Editor and Simulation Engine for Petri Nets:
Renew. In Proc. of ICATPN ’04, volume 3099 of LNCS, pages 484–493. Springer,
2004.
11. K. B. Lassen and S. Tjell. Translating Colored Control Flow Nets into Readable
Java via Annotated Java Workflow Nets. In Proc. of 8th CPN Workshop, 2007.
12. M. Mascheroni, T. Wagner, and L. Wüstenberg. Verifying Reference Nets by
Means of Hypernets: A Plugin for Renew. In Proc. of the PNSE’19, Berichte des
Fachbereichs Informatik, pages 39–54. Universität Hamburg, 2010.
13. K. H. Mortensen. Automatic Code Generation Method Based on Coloured Petri
Net Models Applied on an Access Control System. In Proc. of ICATPN’00, volume
1825 of LNCS, pages 367–386, 2000.
14. S. Philippi. Automatic code generation from high-level Petri-Nets for model driven
systems engineering. Journal of Systems and Software, 79(10):1444 – 1455, 2006.
15. C. Reinke. Haskell-coloured petri nets. In Int. Workshop on Implementation of
Functional Languages, volume 1868 of LNCS, pages 165–180, 1999.
16. K. I. F. Simonsen, L. M. Kristensen, and E. Kindler. Generating Protocol Software
from CPN Models Annotated with Pragmatics. In Formal Methods: Foundations
and Applications, volume 8195 of LNCS, pages 227–242. Springer, 2013.
17. K.I.F. Simonsen. PetriCode: A Tool for Template-based Code Generation from
CPN Models. In Proc. of WS-FMDS 2013, volume 8368 of LNCS, pages 151–163,
2013. Project website: http://www.petricode.org.
18. K.I.F. Simonsen. An Evaluation of Automated Code Generation with the Pet-
riCode Approach. In In Proc. of PNSE ’14, volume 1160 of CEUR Workshop
Proceedings, pages 295–312. CEUR-WS.org, 2014.
19. K.I.F Simonsen and L.M. Kristensen. Implementing the WebSocket Protocol
based on Formal Modelling and Automated Code Generation. In Proc. of IFIP
DAIS’2014, volume 8460 of LNCS, pages 104–118. Springer, 2014.
20. K.I.F. Simonsen, L.M. Kristensen, and E. Kindler. Pragmatics Annotated Coloured
Petri Nets for Protocol Software Generation and Verification. Technical Report 16,
DTU Compute, http://goo.gl/9j6lDz, 2014.