Vol-3170/paper2
Jump to navigation
Jump to search
Paper
| Paper | |
|---|---|
 edit
| |
| description | |
| id | Vol-3170/paper2 |
| wikidataid | Q117351478→Q117351478 |
| title | Partial Specifications of Component-Based Systems using Petri Nets |
| pdfUrl | https://ceur-ws.org/Vol-3170/paper2.pdf |
| dblpUrl | https://dblp.org/rec/conf/apn/HilbrandsBA22 |
| volume | Vol-3170→Vol-3170 |
| session | → |
Partial Specifications of Component-Based Systems using Petri Nets
Partial Specifications of Component-based Systems
using Petri Nets
Bart-Jan Hilbrands1,2 , Debjyoti Bera1 and Benny Akesson1,2
1
ESI (TNO), Eindhoven, the Netherlands
2
University of Amsterdam, Amsterdam, the Netherlands
Abstract
Component-based architectures are commonly used in industry to manage the increasing complexity
of systems. In such architectures, components interact with each other to achieve the desired func-
tionality. They do so by providing and consuming services to and from each other over their defined
interfaces. Interfaces play a key role in managing complexity by abstracting away from implementation
details and describing only externally observable behavior. To describe the behavior of an interface and
analyze them for correctness, formalisms, such as finite state machines and Petri nets, are commonly
used. However, components usually have multiple interfaces and their behavior may depend on each
other. Most approaches so far have focused on fully specifying the behavior of a component as a single
state machine. We consider partial specification of dependencies between interfaces, expressed as a set
of functional constraints. In this paper, we present and formalize three commonly occurring functional
constraints. Algorithms are proposed to generate Petri nets satisfying each of these constraints.
1. Introduction
Systems are becoming increasingly complex, making them challenging to develop, maintain, and
evolve over time [1]. This complexity is usually managed by taking a component-based approach
to achieve modularity [2, 3] by decomposing the system into asynchronously communicating
components. The components provide or consume services to and from each other over interfaces
to realize the functionality of the system. An interface specification must capture, next to a list
of events, also the externally observable behavior by abstracting away from implementation
details. It is common practice in industry to define interfaces in natural text, interface description
languages (IDLs), or in code (header files), focusing mostly on the static structural aspects, e.g.
a list of possible events. Some domain-specific languages (DSLs) exist, such as Component
Modelling and Analysis (ComMA) [4] and Dezyne [5], which capture both the structural and
behavioral aspects of an interface.
Capturing behavioral aspects of an interface, usually as protocol state machines, has many
benefits in a component-based approach. For instance, the behavioral description can be used
as contracts between teams allowing them to work independently, or as contracts to external
suppliers. They may also be used to generate code stubs, or even online test clients or offline test
scenarios to check if the implementation conforms to the specified contracts. Furthermore, since
PNSE’22, International Workshop on Petri Nets and Software Engineering, Bergen, Norway, 2022
" bj.hilbrands@gmail.com (B. Hilbrands)
© 2022 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
CEUR
Workshop
Proceedings
http://ceur-ws.org
ISSN 1613-0073 CEUR Workshop Proceedings (CEUR-WS.org)
21
�Bart-Jan Hilbrands et al. CEUR Workshop Proceedings 21–39
interfaces describe the expected interactions between components of a system, it is valuable
to check their correctness at design time, e.g. if the interactions are free from deadlocks,
livelocks, and unbounded behavior. This allows design errors to be detected early during system
specification rather than later during integration and testing, reducing cost.
A component typically has multiple interfaces, and it is quite common that the behavior
of one interface on a component depends on the state of another. Such dependencies may be
captured as functional constraints defined over states and transitions of one or more protocol
state machines. For example, a transition in one interface may or may not happen if another
interface is in a particular state. Another example could be that a transition in one interface must
be followed by a sequence of transitions in other interfaces. Most work in literature have focused
on defining the complete behavior of a component as one or more state machines. In practice,
defining the complete behavior of a component is usually not possible, due to complexity and
limited knowledge of the implementation. Instead, we focus on the fact that interfaces serve as
abstractions of the underlying component implementation by allowing for non-determinism,
e.g. the response to an initialization request may be either a success or fail, but we do not say
when one or the other is possible. Our goal is to exploit this level of abstraction to capture
partial specifications of a component as functional constraints over one or more interfaces.
The three main contributions of this paper are: 1) A formalization of three types of commonly
occurring functional constraints, namely enabling, disabling, and causal sequence constraints.
The formalization describes how each constraint should limit the behaviour of a set of P/T nets,
each corresponding to a protocol state machine in an interface. 2) A set of assumptions on
specific constraints to avoid creating problematic specifications. 3) A method to represent and
incorporate these functional constraints into an existing Petri net representation of component
interfaces, in our case generated from a ComMA specification, which enables absence of dead-
lock, livelock, and unbounded behavior of dependent interfaces to be verified using reachability
analysis. The method is accompanied by proof sketches, showing that the results produced by
the method satisfy the properties defined in the formalization. Throughout the paper, a case
study of a vending machine is used as a running example to demonstrate the approach.
The rest of the paper is organized as follows. Section 2 presents related work, while Section 3
introduces relevant preliminaries, as well as the vending machine case study that is used as a
running example. In Section 4, a formalization of the three types of constraints is presented.
This is followed by a series of assumptions about the behaviour of a given specification, showing
that some specifications of constraints may cause termination issues. Section 5 continues by
presenting for each type of constraint, an algorithm encoding the constraint, as well as proof
sketches showing that the algorithm produces a Petri net that complies with the properties
defined in Section 4. Finally, conclusions are drawn in Section 6.
2. Related Work
The main goal of this work is to synthesize, for each specified constraint, additional Petri
net constructs between existing nets (each describing an interface protocol state machine) to
constrain the space of possible behaviors in their reachability graph. The challenge is to ensure
that such a graph correctly encodes the specified constraints. Based on such a reachability
22
�Bart-Jan Hilbrands et al. CEUR Workshop Proceedings 21–39
graph, it is possible to verify properties, such as absence of deadlocks, livelocks, and unbounded
behavior, at design time.
Since model checking monolithic models describing a system is typically infeasible due to
state space explosion, a compositional approach is usually taken. Both [6] and [7] propose such
an approach. The work in [8] considers another compositional approach based on interface
compliance to ensure that the behavior of the whole is guaranteed to be correct, i.e. absence
of deadlocks, livelocks and unbounded behavior. In constrast to the work presented in this
paper, all the above approaches focus on fully specifying the behavior of a component as a state
machine. The latter goes even further to generate production code from such models. The work
in [9] is similar to the work presented in this paper in the sense that a partial specification is
translated to a formal specification language in order to do verification. This specification is
given in UML-RT [10], and is translated to a CSP [11] model to verify deadlock-freedom.
There are also several works [12, 13, 14] that propose correct by construction methods to
design component-based systems. Such an approach avoids the drawbacks of having to model
check large models. However, there are two main differences to the approach proposed in this
paper. Firstly, they propose design methods that guarantee certain properties by construction,
such as absence of deadlocks and livelocks. The second difference is once again in the focus on
fully specifying the behavior of a component, as opposed to partial specifications considered in
this paper.
In conclusion, no method currently exists to encode commonly occurring functional con-
straints over interfaces of a component for design-time analysis.
3. Preliminaries
This section introduces the preliminaries for this work. Firstly, Section 3.1 starts off with the
introduction of ComMA, the modelling and analysis framework in which the component and
interfaces specifications are defined. Secondly, relevant Petri net concepts are introduced in
Section 3.2, followed by a description of how ComMA interfaces are currently represented as
Petri nets.
3.1. ComMA Component and Interface Specification
Component Modelling and Analysis (ComMA) [4] is a supporting tool for modelling and analysis
of interfaces in component-based systems. It provides a family of domain-specific languages
for specification of structure and behavior of component interfaces and their constraints from
which documentation, analysis, and monitors can be generated[15]. ComMA is available as an
open-source tool under the name Eclipse CommaSuite1 .
The behaviour of an interface is specified in ComMA as a protocol state machine. Figures 1a
and 1b show two example interfaces, a Service Interface and a User Interface, that belong
to a vending machine component that is used as a running example in this paper. Figure 1a
shows an interface with three states: Off, Operational, and Error. Through this interface, a
technician may turn the machine on or off, and may restock the machine with LoadProduct.
1
https://www.eclipse.org/comma/
23
�Bart-Jan Hilbrands et al. CEUR Workshop Proceedings 21–39
The machine may also go out of order from any state, in which case it can be reset. Figure 1b
shows an interface with the following three states: Uninitialized, Ready and Empty. Initially,
the interface is in the Uninitialized state. After initializing, it is in the ready state. Here,
an Initialized or ResetDone message can be sent, depending on whether the machine was
initialized after a Reset or a SwitchOn. If the machine is out of products, it will go to the
Empty state, and can go back to the Ready state if the machine is restocked.
(a) Protocol of the Service Interface (b) Protocol of the User Interface
1. LoadProduct shall only happen if the User interface is in the Empty state
2. Order shall not happen if the Service interface is in the Error state
3. SwitchOn shall be followed by Initialize followed by Initialized
4. SwitchOn shall only happen if the User interface is in the Uninitialized state
5. Reset shall be followed by Initialize followed by ResetDone
6. Reset shall only happen if the User interface is in the Uninitialized state
(c) Functional constraints on the service and user Interface
Figure 1: Vending machine example.
A ComMA component specification describes how events on one interface depend on events
of other interfaces. These component specifications are referred to as functional constraints.
Functional constraints are of three types. Firstly, the enabling constraint, which defines an
additional enabling condition for transitions that depends on the current state of one or more
other interfaces. For our vending machine, constraints 1, 4 and 6 in Figure 1c are enabling
constraints. Secondly, the disabling constraint, which defines a disabling condition for transitions
that depends on the current state of one or more other interfaces. In Figure 1c, this is constraint
2. Lastly, the causal sequence constraint requires that when certain transitions on one interface
are fired, they are always followed by a sequence of transitions from other interfaces. In our
vending machine example, constraints 3 and 5 fall under this category.
24
�Bart-Jan Hilbrands et al. CEUR Workshop Proceedings 21–39
3.2. Petri Nets
A Petri net is a tuple 𝑁 = (𝑃, 𝑇, 𝐹 ), where 𝑃 is the set of places; 𝑇 is the set of transitions such
that 𝑃 ∩𝑇 = ∅ and 𝐹 is the flow relation 𝐹 ⊆ (𝑃 ×𝑇 )∪(𝑇 ×𝑃 ). We refer to elements from 𝑃 ∪𝑇
as nodes and elements from 𝐹 as arcs. We define the preset of a node 𝑛 as ∙ 𝑛 = {𝑚|(𝑚, 𝑛) ∈ 𝐹 }
and the postset as 𝑚∙ = {𝑛|(𝑚, 𝑛) ∈ 𝐹 }. A finite sequence over a set 𝑆 with length 𝑛 ∈ N is
denoted by 𝜎, where 𝜎 is a function 𝜎 : {1, .., 𝑛} → 𝑆. We denote the set of all finite sequences
over 𝑆 by 𝑆 * . We say that a function 𝑚 : 𝑆 → N over some set 𝑆 is a bag over 𝑆. For some
𝑠 ∈ 𝑆, 𝑚(𝑠) denotes the number of occurrences of s in 𝑚. The set of all bags over 𝑆 is denoted
by 𝐵(𝑆).
A P/T net 𝑁 is a state machine (S-net) iff: ∀𝑡 ∈ 𝑇𝑁 : |∙ 𝑡| ≤ 1 ∧ |𝑡∙ | ≤ 1 and all markings
have exactly one token [16]. This means there is a one-to-one mapping between the states of
the corresponding state machine and places in its S-net representation. Since S-net markings
only have a single token, a place 𝑝 having a token represents the protocol of the interface being
in a state 𝑠.
While open Petri nets (OPNs) [17] are sometimes used to model interfaces and their interac-
tions [14, 12], we do not need them for this paper. This is because the functional constraints
are defined on internal behavior of a single component with multiple interfaces. Communication
with other components through designated interface places introduced by OPNs is hence out
of scope. We therefore drop these designated interface places, leaving us only with interface
skeletons, which we refer to as interface nets. A component is therefore defined as a set of S-Nets
representing the interfaces that it implements. For a component 𝒪, all ⋃︀ interfaces 𝑁 ∈ 𝒪 are
pairwise disjoint. For⋃︀a component 𝒪, 𝑃𝒪 denotes the set of all places 𝑁 ∈𝒪 (𝑃𝑁 ), and 𝑇𝒪 the
set of all transitions 𝑁 ∈𝒪 (𝑇𝑁 ).
Figure 2 shows the interface skeletons of the two vending machine interfaces represented as
S-nets, which is the result of an existing transformation in ComMA. As each transition in Figure
2 represents an event on an interface, we will use the term event and transition interchangeably.
Note that there are no connections between places and transitions in the two interfaces. This is
because the transformation does not consider functional constraints during the transformation.
That is a novel contribution of this paper.
4. Formalization of Functional Constraints
In this section, we formalize the three types of constraints presented in Section 3: 1) Enabling
constraint: an event of an interface can only occur if one or more other interfaces are in a certain
specified state, 2) Disabling constraint: an event of an interface cannot occur if one or more
other interfaces are in a certain specified state, and 3) Causal sequence constraint: An action
must be followed by a sequence of events across multiple interfaces. In this section we will
formalize the three constraints as reachability properties, starting with enabling constraints
in Section 4.1 and continuing with disabling constraints and causal sequence constraints in
Sections 4.2 and 4.3, respectively.
25
�Bart-Jan Hilbrands et al. CEUR Workshop Proceedings 21–39
Figure 2: S-net representations of the Service Interface and User Interface of the Vending Machine
component.
4.1. Enabling Constraint
An enabling constraint for a transition is defined as an additional enabling condition for that
transition based on the current states of one or more other interfaces, i.e. an enabling constraint
on a transition requires places of other interfaces to contain a token in order to be enabled.
Currently, only conjunctive enabling constraints are supported by the encoding method. For
example, the constraint that a token must be in places P and P’ for T to be enabled is supported,
but the constraint requiring a token must be in either P or P’ for T to be enabled is not. While
considering both conjunctive and disjunctive enabling constraints would enable a wider range
of models to be supported, it would also add more complexity to the encoding. It is therefore
something to consider in the future.
Definition 1 (Enabling constraint). Given a Component 𝒪 and a set of transitions 𝑇𝑐 ⊆ 𝑇𝒪 , an
enabling constraint is defined as
𝐶𝑒 : 𝑇𝑐 → 𝑃𝒪
A component 𝒪 satisfies a set of constraints 𝐶𝑒 iff for any given transition 𝑡 ∈ 𝑇𝑐 and marking
𝑚 ∈ 𝐵(𝑃𝒪 ):
𝑡
if 𝑚−→ then ∀𝑝 ∈ 𝐶𝑒 (𝑡) : 𝑚(𝑝) = 1
Given constraint 1 of Figure 1c, we can then define 𝐶𝑒 (LoadProduct) = {Empty}.
26
�Bart-Jan Hilbrands et al. CEUR Workshop Proceedings 21–39
4.2. Disabling Constraint
A disabling constraint for a transition is also defined as an additional enabling condition for
that transition based on the current states of one or more other interfaces. Contrary to the
enabling constraint, places must now act as a disabling condition. A disabling constraint on
a transition hence requires that this transition is disabled if a set of places in other interfaces
contain a token.
Definition 2 (Disabling constraint). Given a Component 𝒪 and a set of transitions 𝑇𝑐 ⊆ 𝑇𝒪 , a
disabling constraint is defined as
𝐶𝑑 : 𝑇𝑐 → 𝑃𝒪
A component 𝒪 satisfies a set of constraints 𝐶𝑑 iff for any given transition 𝑡 ∈ 𝑇𝑐 and marking
𝑚 ∈ 𝐵(𝑃𝒪 ):
𝑡
if 𝑚−→ then ∀𝑝 ∈ 𝐶𝑑 (𝑡) : 𝑚(𝑝) = 0
Given constraint 2 of Figure 1c, we can then define 𝐶𝑑 (Order) = {Error}.
4.3. Causal Sequence Constraint
A causal sequence constraint requires that whenever a certain transition on an interface is fired
then a sequence of transitions on other interfaces of that component is executed, and no other
firing sequence is possible.
Definition 3 (Causal sequence constraint). Given a Component 𝒪 and a set of transitions 𝑇𝑐 ⊆
𝑇𝒪 , a causal sequence constraint is defined as follows:
𝐶𝑠 : 𝑇𝑐 → 𝑇 *
A component satisfies a causal sequence constraint 𝐶𝑠 iff for any given transition 𝑡 ∈ 𝑇𝑐 and
marking 𝑚 ∈ 𝐵(𝑃𝒪 ):
𝑡
if 𝑚−→ 𝑚′ then:
𝜎 𝜎′
∃𝑚′ −→ such that 𝜎 = 𝐶𝑠 (𝑡) ∧ ¬∃𝑚′ −→ such that 𝜎 ′ ̸= 𝜎
Given constraint 3 of Figure 1c, we can then define the causal sequence constraint
𝐶𝑠 (SwitchOn) = ⟨Initialize, Initialized⟩. For a component 𝒪 and a transition 𝑡 ∈ 𝑇𝒪 , if
𝐶𝑠 (𝑡) ̸= 𝜖, we say that 𝑡 is an activation transition of a sequence. For constraints 3 and 5 of Fig-
ure 1c, these would be SwitchOn and Reset. Any transition 𝑡𝑛 ∈ 𝐶𝑠 (𝑡) where 0 ≤ 𝑛 ≤ |𝐶𝑠 (𝑡)|,
is a consequence transition. These would be Initialize, Initialized, and ResetDone belonging
to constraint 3 and 5. We require that an activation transition cannot belong to more than one
causal sequence constraint of a component 𝒪. Furthermore, a transition cannot be an activation
transition if it is also a consequence transition. If a transition is neither a consequence nor an
activation transition of any defined causal sequence constraint of component O, we refer to it as
27
�Bart-Jan Hilbrands et al. CEUR Workshop Proceedings 21–39
a free transition. The Order, Deactivate, and LoadProduct transitions are free transitions in
our example. For two consequence transitions 𝑡𝑛 , 𝑡𝑛+1 ∈ 𝐶𝑠 (𝑡) where 0 ≤ 𝑛 < |𝐶𝑠 (𝑡)|, we say
that 𝑡𝑛+1 is a sequence successor of 𝑡𝑛 , and that 𝑡𝑛 is a sequence predecessor of 𝑡𝑛+1 . For example,
ResetDone is a sequence successor of Initialize. It is important to note that consequence
transitions can only be fired after the firing of one of its predecessors, meaning they cannot
be fired independently outside the context of a sequence. Furthermore, only one sequence
may be active at the same time, meaning that after some activation transition 𝑡 fires, any other
activation transition cannot be enabled.
There are some constraint specification that could make the encoding more complex, and
should be considered separately. These cases are now introduced, starting off with the notion of
overlapping and diverging causal sequences. It is possible that a sequence of consequence transi-
tions of two or more causal sequence constraints overlap. That is, for two activation transitions
𝑡 and 𝑡′ , and some sequence of consequence transitions 𝜎, 𝜎 may be a subsequence of both 𝐶𝑠 (𝑡)
and 𝐶𝑠 (𝑡′ ). Whenever a set of sequences share a subsequence of consequence transitions, we
say that the sequences are overlapping. If a set of sequences has 𝜎 as a common subsequence,
we say that the sequences overlap on 𝜎. For two sequences 𝐶𝑠 (𝑡) = ⟨𝑡0 , 𝑡1 , 𝑡2 , 𝑠0 , 𝑠1 , 𝑡3 ⟩ and
𝐶𝑠 (𝑡′ ) = ⟨𝑡′0 , 𝑡′1 , 𝑠0 , 𝑠1 , 𝑡′2 ⟩, this is illustrated in Figure 3. The behaviour of the sequences shown
in Figure 3 is clear, at least until we reach transition 𝑠1. At this point, 𝑠1 is followed by either
transition 𝑡3 or 𝑡2′ , depending on which sequence is active. In this case, we say that the set of
sequences are diverging, and that 𝑠1 is a divergence point.
t0 t1 t2 s0 s1 t3
t0’ t1’ t2’
Figure 3: Overlapping and diverging sequences
When specifying causal sequence constraints, it also possible that there are recurring elements
in the sequence. While a sequence is active, it is then possible that transitions may have to
followed by different transitions in the context of this single sequence. For example, in the
sequence 𝐶𝑠 (𝑡) = ⟨𝑡0 , 𝑡1 , 𝑡2 , 𝑡0 , 𝑡3 ⟩, the first time 𝑡0 is taken it is followed by 𝑡1 and the second
time, by 𝑡3 . Such sequences are referred to as multi-stage sequences, but are out of scope in
this paper. Every sequence considered in this paper is a single-stage sequence, as there is no
divergence within the context of a single sequence. For more information about multi-stage
sequences, refer to [18].
4.4. Assumptions on Functional Constraints
It is possible that adding functional constraints to a component specification causes termination
problems, such as deadlock or livelock.
In the proof-sketches of Section 5, we reason about the enabledness of transitions belonging
to the Petri nets produced by the encoding algorithms. If a given specification has inherent
28
�Bart-Jan Hilbrands et al. CEUR Workshop Proceedings 21–39
termination problems, it could cause certain transitions to be disabled indefinitely as a result of
the specified functional constraints, regardless of how they are encoded as a Petri net. Because
this would create problems for the proof sketches, this section introduces three assumptions on
the behaviour of a given specification.
Let 𝐶𝑠 (𝑡) = ⟨𝑡0 , ..., 𝑡𝑛 ⟩ where 𝑛 ∈ 𝒩 be causal sequence constraint on a transition 𝑡 belonging
to an interface 𝑁 . Whenever a transition 𝑡𝑖 ∈ 𝐶𝑠 (𝑡) where 0 ≤ 𝑖 ≤ 𝑛 fires, the transition 𝑡𝑖+1
belonging to an interface 𝑁 ′ must be enabled in the resulting marking 𝑀 . Because 𝑁 ′ is an
S-net, 𝑡𝑖+1 will have exactly one place 𝑝 belonging to 𝑁 ′ in its preset. For 𝑡𝑖+1 to be enabled, 𝑝
must therefore have a token in 𝑀 , which may not always be the case. In other words, after 𝑡𝑖
fires, 𝑁 ′ may not be in a state in which 𝑡𝑖+1 can be fired.
Recall the causal sequence constraints 3 and 5, and enabling constraints 4 and 6 of Figure 1c.
If these two enabling constraints were absent, it would be possible for SwitchOn and Reset to
fire while the place Uninitialized does not have a token. If these transitions were to fire in this
case, the only transition that is allowed to be enabled in the resulting marking is Initialize, as
it is the sequence successor of both of these transitions. However, since Uninitialized has no
token, and is in the preset of Initialize, there is no way for Initialize to be enabled, resulting
in a deadlock. Assumption 1 formalizes this by requiring that after a consequence or activation
transition fires, the interface that its sequence successor 𝑡𝑠𝑢𝑐𝑐 belongs to is in a state where
𝑡𝑠𝑢𝑐𝑐 is enabled.
Assumption 1. Let 𝑡 be an activation transition for a causal sequence 𝐶𝑠 (𝑡) = ⟨𝑡0 , ..., 𝑡𝑛 ⟩ where
𝑛 ∈ N. For any marking 𝑚 that is the result of the firing of 𝑡: 𝑡0 is enabled in m. For any marking
𝑚′ that is the result of the firing of 𝑡𝑖 ∈ 𝐶𝑠 (𝑡) where 0 ≤ 𝑖 ≤ |𝐶𝑠 (𝑡)| − 1: 𝑡𝑖+1 is enabled in 𝑚′ .
Enabling and disabling constraints combined with causal sequence constraints may also lead
to situations in which it is impossible to satisfy all constraints. Consider the vending machine
example. Suppose that we were to define an enabling constraint requiring the Service Interface
to be in the Off state for Initialize to be enabled. As Initialize is a sequence successor of
Reset and SwitchOn, both of which transition the Service interface to the Operational state,
firing either Reset or SwitchOn would lead to deadlock. Assumptions 2 and 3 formalize this
for the enabling and disabling constraint, respectively.
Assumption 2. Let 𝑡 be an activation transition for a causal sequence 𝐶𝑠 (𝑡) = ⟨𝑡0 , ..., 𝑡𝑛 ⟩ where
𝑛 ∈ N. For any marking 𝑚 that is the result of the firing of 𝑡:∀𝑐 ∈ 𝐶𝑒 (𝑡0 ) : 𝑚(𝑐) = 1. For
any marking 𝑚′ that is the result of the firing of 𝑡𝑖 ∈ 𝐶𝑠 (𝑡) where 0 ≤ 𝑖 ≤ |𝐶𝑠 (𝑡)| − 1, and the
transition 𝑡𝑖+1 ∈ 𝐶𝑠 (𝑡) belonging to some interface 𝑁 : ∀𝑐 ∈ 𝐶𝑒 (𝑡𝑖+1 ) : 𝑚′ (𝑐) = 1.
Assumption 3. Let 𝑡 be an activation transition for a causal sequence 𝐶𝑠 (𝑡) = ⟨𝑡0 , ..., 𝑡𝑛 ⟩ where
𝑛 ∈ N. For any marking 𝑚 that is the result of the firing of 𝑡: ∀𝑐 ∈ 𝐶𝑑 (𝑡0 ) : 𝑚(𝑐) = 0. For
any marking 𝑚′ that is the result of the firing of 𝑡𝑖 ∈ 𝐶𝑠 (𝑡) where 0 ≤ 𝑖 ≤ |𝐶𝑠 (𝑡)| − 1, and the
transition 𝑡𝑖+1 ∈ 𝐶𝑠 (𝑡) belonging to some interface 𝑁 : ∀𝑐 ∈ 𝐶𝑑 (𝑡𝑖+1 ) : 𝑚′ (𝑐) = 0.
5. Encoding Constraints as Petri Nets
Given the S-net representation of a set of interface skeletons, and a set of functional constraints,
we will now present algorithms to add transitions and places to existing interface nets such that
29
�Bart-Jan Hilbrands et al. CEUR Workshop Proceedings 21–39
they satisfy a set of given functional constraints. There are obviously a lot of different ways
to this. However, for the purposes of this paper, which is gaining access to the reachability
graph of a given component and verifying the absence of deadlock, livelock and unbounded
behaviour, only one possible encoding has been proposed. Making a comparison between
different encoding is something to consider for the future.
Figure 4 shows an example of adding functional constraints described earlier in Section 3.1 to
a set of interface nets described in Figure 2. Throughout this section, different parts of Figure 4
will be highlighted and discussed to exemplify the output of the method.
Figure 4: Resulting Petri net after applying the method in this section on the two vending machine
interfaces
5.1. Enabling constraint
For a component 𝒪, and a set of enabling constraints defined by 𝐶𝑒 , Algorithm 1 generates a
Petri net that encodes the constraints defined in 𝐶𝑒 . The algorithm is fairly straightforward:
Line 3 creates bidirectional arcs between 𝑡 and all 𝑝 ∈ 𝐶𝑒 (𝑡) in order to enforce the constraints
of 𝐶𝑒 (𝑡). The arcs are bidirectional to ensure that when 𝑡 fires, the token in 𝑝 is not consumed.
We can see how this works out for the enabling constraints defined on the interfaces of our
vending machine component. In Figure 4, we can see a bidirectional arc created between the
LoadProduct transition, and the Empty place to satisfy constraint 1 of Figure 1c. Similarly,
we can see a bidirectional arc created between both the SwitchOn and Reset transtition, and
the Uninitialized place to satisfy constraints 4 and 6. Next, Lemma 1 shows that Algorithm 1
encodes enabling constraints such that the reachability property in Definition 1 is satisfied.
30
�Bart-Jan Hilbrands et al. CEUR Workshop Proceedings 21–39
1 foreach transition 𝑡 ∈ 𝑇𝒪 do
2 foreach place 𝑝 ∈ 𝐶𝑒 (𝑡) do
3 create bidirectional arc(p, t )
4 end
5 end
Algorithm 1: Enabling Constraints
Lemma 1. The reachability property defined for the enabling constraint in Definition 1 always
holds for a component 𝒪 after applying Algorithm 1 on 𝒪.
Proof sketch. Let 𝒪 be a component with the constraints 𝐶𝑒 , and 𝑡 a transition of 𝑇𝒪 . Line 3
guarantees a bidirectional arc is created between 𝑡 and each of the places in 𝐶𝑒 (𝑡), meaning
that all of the places in 𝐶𝑒 (𝑡) are in the preset of 𝑡. Therefore, 𝑡 can only fire if all places in
𝐶𝑒 (𝑡) have a token, as required by the property in Definition 1.
5.2. Disabling Constraint
The algorithm for disabling constraints is similar to that of the enabling constraint, which
makes sense as the disabling constraint is essentially its inverse. When 𝐶𝑑 (𝑡) = {𝑝} for some
transition 𝑡 and a place 𝑝, instead of enabling 𝑡 when 𝑝 has a token, 𝑡 must now be disabled
instead. While using inhibitor arcs is an intuitive solution to this problem, we restrict ourselves
to P/T nets to support reachability analysis with a broader range of tools. Instead, complement
places are be used, which allows us to model the functionality of inhibitor arcs. We can do this
because all interfaces are S-nets and therefore safe [19]. For a place 𝑝, its complement place
𝑝
¯ has a token only if 𝑝 does not. With this behaviour, a bidirectional arc can then be created
between a transition 𝑡 and the complement place 𝑝 ¯ of a place 𝑝 ∈ 𝐶𝑑 (𝑡). For a component 𝒪,
and a set of disabling constraints defined by 𝐶𝑑 , Algorithm 2 generates a Petri net that encodes
the constraints defined in 𝐶𝑑 .
Line 3-6 are responsible for creating complement places, and making sure the complement
places have the correct number of initial tokens, depending on whether 𝑝 has a token initially.
Lines 7-10 then make sure that the complement places are correctly updated as the net executes.
This is done by creating arcs from the complement place of 𝑝, to each transition 𝑝𝑡 in the preset
of 𝑝, and by creating arcs from each transition 𝑝𝑡 in the postset of 𝑝, to the complement place of
𝑝. Line 11 then creates a bidirectional arc that ensures that a transition can only be enabled
if the right complement place has a token. It is shown in Lemma 2 that Algorithm 2 encodes
disabling constraints in a way that satisfies the reachability property in Definition 2.
Lemma 2. The reachability property defined for the disabling constraint in Definition 2 always
holds for a component 𝒪 after applying Algorithm 2 on 𝒪.
Proof sketch. Let 𝒪 be a component with the constraints 𝐶𝑑 , and 𝑡 be a transition of 𝑇𝒪 .
Because of Lines 3-6, every place in 𝐶𝑑 (𝑡) has a complement place, with Lines 3-4 ensuring that
the complement place has no token if the corresponding place has a token in the initial marking.
For any place 𝑝 in 𝐶𝑑 (𝑡), its complement place 𝑝 ¯ can only have a token if 𝑝 has no token, as
31
�Bart-Jan Hilbrands et al. CEUR Workshop Proceedings 21–39
1 foreach transition 𝑡 ∈ 𝑇𝒪 do
2 foreach place 𝑝 ∈ 𝐶𝑑 (𝑡) do
3 if 𝑚0 (𝑝) = 1 then
4 create place(𝑝 ¯, 0 tokens)
5 else
6 create place(𝑝 ¯, 1 token)
7 foreach place 𝑝𝑡 ∈ ∙ 𝑝 do
8 create arc(𝑝 ¯, pt )
9 end
10 foreach place 𝑝𝑡 ∈ 𝑝∙ do
11 create arc(pt, 𝑝 ¯)
12 end
13 create bidirectional arc(𝑐𝑜𝑚𝑝𝑙𝑒𝑚𝑒𝑛𝑡𝑝 , t )
14 end
15 end
Algorithm 2: Disabling Constraints
by Lines 7-8, any transition in the preset of 𝑝 removes a token from 𝑝¯, and by Lines 10-11, any
transition in the postset of 𝑝 adds a token to 𝑝¯. With Line 13 then guaranteeing that each of
these complement places are in the preset of 𝑡, 𝑡 can thus only be enabled if for all 𝑝 in 𝐶𝑑 (𝑡), 𝑝
has no token, as required by Definition 2.
We demonstrate Algorithm 2 constraint 2 of Figure 1c. Figure 4 shows that there now exists
a complement place for the Error state, and that there is a bidirectional arc created between
this complement place and the Order transition. The only transition that produces a token
to the Error place, OutOfOrder, removes a token from the complement place, and likewise
the only transition that removes a token from the Error place, Reset, produces a token to the
complement place.
5.3. Causal Sequence constraints
For a component 𝒪 and a causal sequence constraint 𝐶𝑠 (𝑡) = ⟨𝑡0 , ..𝑡𝑛 ⟩, the following two things
have to be guaranteed by Algorithm 3 in order to satisfy the property given in Definition 3. Firstly,
after 𝑡 fires, all free transitions must be disabled until the last transition in 𝐶𝑠 (𝑡) fires. Secondly,
any transition 𝑡𝑖 ∈ 𝐶𝑠 (𝑡) with 1 < 𝑖 < |𝐶𝑠 (𝑡)|, must only be enabled after 𝑡𝑖−1 ∈ 𝐶𝑠 (𝑡) fires.
The first requirement is satisfied by introducing a disabler place with a token in the initial
marking. Any free transition has a bidirectional arc to this disabler place, which prevents
them from being enabled whenever the disabler place has no token. All activation transitions
furthermore have an incoming arc coming from this disabler, disabling all free transitions, as
well as any other activation transitions. The final transition of each sequence is then responsible
for producing a token back to the disabler place. The downside of this approach is that by
connecting many transitions of different interfaces to one place, we go against the locality
principle of P/T nets. Structural reduction methods that can be used to reduce the size of
given P/T nets, often rely on exploiting locality properties, are therefore less applicable to nets
32
�Bart-Jan Hilbrands et al. CEUR Workshop Proceedings 21–39
produced by this method.
The second requirement is satisfied using distinct enabler places that each consequence
transition will have in its preset. Enabler places have no token in the initial marking, and the
algorithm ensures that the enabler place of a consequence transition 𝑡 can only receive a token
from the sequence predecessor of 𝑡. However, if there are divergence points this is not enough,
and for such cases a decision place is introduced. For a transition 𝑡, this decision place has a
transition referred to as decision transitions in its postset for each possible sequence successors
of 𝑡. Each of these transitions put a token in the enabler place of its corresponding sequence
successor. To know which of these transitions must be enabled, an active place is introduced for
each defined sequence. Each activation transition 𝑡 puts a token in a place corresponding to
the sequence 𝐶(𝑡), while the last transition of 𝐶(𝑡) removes it. By then creating a bidirectional
arc between each of the transitions in the postset of the decision place of 𝑡, only the correct
decision transition is enabled. Introducing these additional places that indicate which sequence
is active does introduce another problem. Ambiguity may now arise when when a transition is
the final transition of multiple sequences, or is the final transition of one sequence while being
a non-final transition of another. Therefore, the decision place must also be used in such cases.
For a transition 𝑡 and its decision place 𝑝, there is a transition for each of the sequences that has
𝑡 as its final transition in the postset of 𝑝. Each of these transitions then remove a token from
the corresponding active place.
As an example, Figure 4 shows how the causal sequence constraints 3 and 5 of Figure 1c
are encoded. In our specification, Initialize is a divergence point, as it is followed by either
a ResetDone or Initialized. We thus need two places indicating which sequence is active,
which are Reset_Stage0 and SwitchOn_Stage0, present on the right of Figure 4. We can
see that the activation transitions SwitchOn and Reset, put a token in SwitchOn_Stage0
and Reset_Stage0, respectively. Initialized then removes the token from SwitchOn_Stage0,
as it is the final transition of the sequence activated by SwitchOn. Likewise, ResetDone
removes the token from Reset_Stage0, as it is the final transition of the sequence activated
by Reset. As both of these transitions are final transitions, they add a token to the disabler
place. Because Initialize is a divergence point, we can see that it now has Initialize_choice
in its postset, shown on the right side of Figure 4. In the postset of this place, we can see a
transition corresponding to each of the two defined sequences. choice_Reset_stage0 has a
bidirectional arc to Reset_Stage0, while choice_SwitchOn_stage0 has a bidirectional arc
to SwitchOn_Stage0. For each of the consequence transitions Initialize, Initialized and
ResetDone, we can see that there is now an enabler place in their preset. Only the sequence
predecessors, which for Initialize are Reset and SwitchOn, put a token in these places. For
the divergence point Initialize, we can see that the decision transitions in the postset of
Initialize_choice are now responsible for this, rather than Initialize itself.
It now needs to be shown that after applying Algorithm 3, the resulting net satisfies any
single-stage causal sequence constraint. The following places and transitions are used in the
proof sketches of this section. For a consequence transition 𝑡𝑛 , 𝑝𝑑𝑒𝑐𝑖𝑠𝑖𝑜𝑛
𝑛 refers to the decision
place of 𝑡𝑛 created on Line 16 of Algorithm 3. Every transition 𝑡 in the postset of 𝑝𝑑𝑒𝑐𝑖𝑠𝑖𝑜𝑛
𝑛 is a
decision transition of 𝑡𝑛 . For a sequence 𝑠, 𝑠𝑎𝑐𝑡𝑖𝑣𝑒 denotes the place created on Line 3, that is
used to indicate whether or not the sequence 𝑠 is currently active. 𝑚𝑎𝑐𝑡 denotes the marking
that is the result the firing of an activation transition 𝑡 for a sequence 𝐶𝑠 (𝑡).
33
�Bart-Jan Hilbrands et al. CEUR Workshop Proceedings 21–39
1 create place(disabler, 1 token);
2 foreach sequence 𝑠 do
3 create place(𝑠𝑎𝑐𝑡𝑖𝑣𝑒 , 0 tokens)
4 end
5 foreach transition 𝑡 ∈ 𝑇𝒪 do
6 if 𝑡 is free then
7 create bidirectional arc(disabler, t )
8 else if t is an activation transition for a sequence s starting with 𝑡0 then
9 create place(𝑡0 _enabler, 0 tokens);
10 create arc(𝑡0 _enabler, 𝑡0 );
11 create arc(t, 𝑡0 _enabler );
12 create arc(disabler, t );
13 create arc(t, 𝑠𝑎𝑐𝑡𝑖𝑣𝑒 )
14 else
15 if 𝑡 is a divergence point then
16 create place(𝑡𝑑𝑒𝑐𝑖𝑠𝑖𝑜𝑛 , 0 tokens);
17 create arc(𝑡, 𝑡𝑑𝑒𝑐𝑖𝑠𝑖𝑜𝑛 );
18 foreach successor 𝑠𝑢𝑐𝑐 ∈ 𝑇𝒪 , where 𝑠𝑢𝑐𝑐 is a successor of 𝑡, and 𝑠𝑢𝑐𝑐 belongs
to the sequence 𝑠 do
19 create transition(𝑡𝑠𝑢𝑐𝑐 );
20 create arc(𝑡𝑑𝑒𝑐𝑖𝑠𝑖𝑜𝑛 , 𝑡𝑠𝑢𝑐𝑐 );
21 create bidirectional arc( 𝑠𝑎𝑐𝑡𝑖𝑣𝑒 , 𝑡𝑠𝑢𝑐𝑐 );
22 if enabler place of successor(t ) does not exist then
23 create place(successor(t )𝑒𝑛𝑎𝑏𝑙𝑒𝑟 , 0 tokens);
24 create arc(successor(t )𝑒𝑛𝑎𝑏𝑙𝑒𝑟 , successor(t ));
25 create arc(𝑡𝑠𝑢𝑐𝑐 , successor(t )𝑒𝑛𝑎𝑏𝑙𝑒𝑟 )
26 end
27 foreach sequence 𝑠, where 𝑡 is the final transition of 𝑠 do
28 create transition(𝑓 𝑖𝑛𝑎𝑙𝑠 );
29 create arc(𝑡𝑑𝑒𝑐𝑖𝑠𝑖𝑜𝑛 , 𝑓 𝑖𝑛𝑎𝑙𝑠 );
30 create arc(𝑠𝑎𝑐𝑡𝑖𝑣𝑒 , 𝑓 𝑖𝑛𝑎𝑙𝑠 );
31 create arc(𝑓 𝑖𝑛𝑎𝑙𝑠 , disabler )
32 end
33 else
34 if 𝑡 is the last transition of the sequence 𝑠 then
35 create arc(𝑡, disabler );
36 create arc(𝑠𝑎𝑐𝑡𝑖𝑣𝑒 , 𝑡);
37 else
38 if if enabler place of successor(t ) does not exist then
39 create place(successor(t )𝑒𝑛𝑎𝑏𝑙𝑒𝑟 , 0 tokens);
40 create arc(successor(t )𝑒𝑛𝑎𝑏𝑙𝑒𝑟 , successor(t ));
41 create arc(𝑡, successor(t )𝑒𝑛𝑎𝑏𝑙𝑒𝑟 )
42 end
Algorithm 3: Causal Sequence Constraints
34
�Bart-Jan Hilbrands et al. CEUR Workshop Proceedings 21–39
Lemma 3. The first transition of 𝐶𝑠 (𝑡), 𝑡0 is enabled in the marking 𝑚𝑎𝑐𝑡 . For the enabledness
of 𝑡0 belonging to an interface 𝑁 , we must consider the following places its preset in the marking
𝑚𝑎𝑐𝑡 :1) Exactly one place 𝑝 ∈ 𝑃𝑁 . This is because 𝑡′ can only belong to one interface, 𝑁 , and has
only one place in its preset while belonging to 𝑁 , as 𝑁 is an S-net, 2) A set of places 𝑐 ∈ 𝐶𝑒 (𝑡0 ),
3) A set of places 𝑐′ ∈ 𝐶𝑑 (𝑡0 ), 4) 𝑝𝑒0 , which is the enabler place of 𝑡0 introduced by Algorithm 3 on
either Line 23 or 39.
Proof sketch. Lines 9 and 10 in Algorithm 3 guarantee that the first consequence transition
of a sequence, 𝑡0 , has an enabler place 𝑝𝑒0 without an initial token in its preset. Line 11 then
guarantees 𝑝𝑒0 is in the postset of the activation transition 𝑡. Using Assumption 1, we can
assume that 𝑚𝑎𝑐𝑡 (𝑝) = 1. Using Assumption 2, we can furthermore assume that for all places
𝑐 ∈ 𝐶𝑒 (𝑡0 ), 𝑚𝑎𝑐𝑡 (𝑐) = 1. Lastly, using Assumption 3, we can assume that for all places
𝑐′ ∈ 𝐶𝑑 (𝑡0 ), 𝑚𝑎𝑐𝑡 (𝑐′ ) = 0. Since 𝑝𝑒0 is in the postset of the activation transition 𝑡, 𝑝𝑒0 also has a
token in 𝑚𝑎𝑐𝑡 . Therefore 𝑡0 is enabled in 𝑚𝑎𝑐𝑡 .
Lemma 4. Let 𝑡 be an activation transition for a sequence 𝐶𝑠 (𝑡), whose firing leads to the marking
𝑚𝑎𝑐𝑡 . Any consequence transition 𝑡′ that is not 𝑡0 is disabled in 𝑚𝑎𝑐𝑡 .
To show that 𝑡′ belonging to an interface 𝑁 is disabled in 𝑚𝑎𝑐𝑡 , we only have to look at the
place 𝑝′𝑒 , which is the enabler place of 𝑡′ introduced by Algorithm 3 on either Line 23 or 39.
Proof sketch. Lines 23 and 24, as well as Lines 39 and 40, guarantee that any consequence
transition 𝑡′ has an enabler place in its preset without a token in the initial marking. Because of
Line 41, this enabler place 𝑝′𝑒 is not in the postset of 𝑡, but rather in the postset of its predecessor
transition 𝑡𝑝𝑟𝑒𝑑 if 𝑡𝑝𝑟𝑒𝑑 is not a divergence point. If 𝑡𝑝𝑟𝑒𝑑 is a divergence point, Line 25 then
ensures 𝑝′𝑒 is in the postset of a the decision transitions of 𝑡𝑝𝑟𝑒𝑑 . There are no other lines that
create transitions that are in the preset of 𝑝′𝑒 , which means means that 𝑝′𝑒 cannot have a token
in 𝑚𝑎𝑐𝑡 . Therefore, 𝑡′ is disabled in 𝑚𝑎𝑐𝑡 .
Lemma 5. Any free transition 𝑡𝑓 𝑟𝑒𝑒 or activation transition 𝑡𝑎𝑐𝑡 cannot be enabled in 𝑚𝑎𝑐𝑡 . To
show that both 𝑡𝑓 𝑟𝑒𝑒 and 𝑡𝑎𝑐𝑡 belonging an interface 𝑁 are disabled in 𝑚𝑎𝑐𝑡 , we only have to look
at the disabler 𝑝𝑑 introduced by Algorithm 3 on Line 1.
Proof sketch. Line 7 guarantees 𝑡𝑓 𝑟𝑒𝑒 has the disabler place 𝑝𝑑 in its preset, Line 12 then
guarantees that 𝑡𝑎𝑐𝑡 has the disabler place in its preset. Because there is no step in the algorithm
creating an arc from 𝑡𝑎𝑐𝑡 to 𝑝𝑑 , 𝑡𝑎𝑐𝑡 never has 𝑝𝑑 in its postset. Line 1 guarantees that 𝑝𝑑 has a
token in the initial marking. This guarantees only activation transitions can remove a token
from 𝑝𝑑 , while Lines 31 and 35 guarantee that the last consequence transitions of a sequence
can produce a token to 𝑝𝑑 . Because we assume that no sequence is currently active, 𝑝𝑑 therefore
has a token. Therefore, after the firing of 𝑡 that results in the marking 𝑚𝑎𝑐𝑡 , the disabler place
𝑝𝑑 does not have a token in 𝑚𝑎𝑐𝑡 . Therefore, 𝑡𝑓 𝑟𝑒𝑒 and 𝑡𝑎𝑐𝑡 are disabled in 𝑚𝑎𝑐𝑡 .
Lemma 6. For any transition 𝑡𝑛 ∈ 𝐶𝑠 (𝑡), where 0 ≤ 𝑛 ≤ |𝐶𝑠 (𝑡)| − 1, and 𝑡 is an activation
transition, and 𝑡𝑛 is not a divergence point: In any given marking 𝑚′ that is the result of the
firing of 𝑡𝑛 , the only transition enabled afterwards is 𝑡𝑛+1 ∈ 𝐶𝑠 (𝑡). For the enabledness of 𝑡𝑛+1
belonging to an interface 𝑁 , we consider the following places in its preset in the marking 𝑚′ :
1) Exactly one place 𝑝 ∈ 𝑃𝑁 , 2)A set of places 𝑐 ∈ 𝐶𝑒 (𝑡𝑛+1 )., 3)A set of places 𝑐′ ∈ 𝐶𝑑 (𝑡𝑛+1 ),
4) 𝑝𝑒𝑛+1 , which is the enabler place of 𝑡′ introduced by Algorithm 3 on either Line 23 or 39.
35
�Bart-Jan Hilbrands et al. CEUR Workshop Proceedings 21–39
Proof sketch. Line 25 guarantees that the enabler place of 𝑡𝑛+1 , 𝑝𝑒𝑛+1 , is in the postset of 𝑡𝑛 .
Line 24 furthermore guarantees that there is an arc going from 𝑝𝑒𝑛+1 to 𝑡𝑛+1 . Because 𝑁 is an
S-Net, only one place belonging to 𝑁 can have a token. Using Assumption 1, we can assume
that this place is 𝑝, and that therefore 𝑚′ (𝑝) = 1. Using Assumption 2, we can furthermore
assume that for all places 𝑐 ∈ 𝐶𝑒 (𝑡𝑛+1 ), 𝑚′ (𝑐) = 1. Lastly, using Assumption 3, we can assume
that for all places 𝑐′ ∈ 𝐶𝑑 (𝑡𝑛+1 ), 𝑚′ (𝑐′ ) = 0. As 𝑝𝑒𝑛+1 is in the postset of 𝑡𝑛 , 𝑝𝑒𝑛+1 has a token
in 𝑚′ . Furthermore, since 𝑡𝑛 is not a divergence point and therefore has exactly one successor,
it has exactly one enabler place 𝑝𝑒𝑛+1 in its postset. Any other enabler place therefore cannot
have a token while 𝑝𝑒𝑛+1 does. Therefore, only 𝑡𝑛+1 is enabled in 𝑚′ .
Lemma 7. For any transition 𝑡𝑛 ∈ 𝐶𝑠 (𝑡), where 0 ≤ 𝑛 ≤ |𝐶𝑠 (𝑡)|−1, 𝑡 is an activation transition,
and 𝑡𝑛 is a divergence point: There is a decision transition 𝑡′ of 𝑡𝑛 whose firing leads to a marking
𝑚 in which only 𝑡𝑛+1 is enabled.
For the enabledness of 𝑡𝑛+1 belonging to an interface 𝑁 , we consider the following places in
its preset in the marking 𝑚: 1) Exactly one place 𝑝 ∈ 𝑃𝑁 , 2) A set of places 𝑐 ∈ 𝐶𝑒 (𝑡𝑛+1 ), 3) A
set of places 𝑐′ ∈ 𝐶𝑑 (𝑡𝑛+1 ), 4) 𝑝𝑒𝑛+1 , which is the enabler place of 𝑡𝑛+1 introduced by Sequence
Algorithm 2.
Proof sketch. Line 19 ensures there exists a decision transition 𝑡′ of 𝑡𝑛 for each sequence
successor of 𝑡𝑛 . Because of Line 25, 𝑝𝑒𝑛+1 is in the postset of 𝑡′ . For the place 𝑝 ∈ ∙ 𝑡𝑛+1 , using
Assumption 1, we can assume that 𝑚(𝑝) = 1. Using Assumption 2, we can furthermore assume
that for all places 𝑐 ∈ 𝐶𝑒 (𝑡𝑛+1 ), 𝑚(𝑐) = 1. Lastly, using Assumption 3, we can assume that for
all places 𝑐′ ∈ 𝐶𝑑 (𝑡𝑛+1 ), 𝑚(𝑐′ ) = 0. Because 𝑝𝑒𝑛+1 is in the postset of 𝑡′ , 𝑝𝑒𝑛+1 will also have a
token in the marking 𝑚. Therefore, 𝑡𝑛+1 is enabled in 𝑚.
Line 20 then ensures that 𝑝𝑑𝑒𝑐𝑖𝑠𝑖𝑜𝑛
𝑛 is in the preset of each decision transition. This means
that if one of these decision transitions fires, none of the other decision transitions are enabled
in the resulting marking. Because any other decision transition could not have fired, any other
consequence transition cannot have a token in its enabling place. Therefore, 𝑡𝑛+1 is the only
transition enabled in 𝑚.
Lemma 8. For any transition 𝑡𝑛 ∈ 𝐶𝑠 (𝑡), where 0 ≤ 𝑛 ≤ |𝐶𝑠 (𝑡)|−1, 𝑡 is an activation transition,
and 𝑡𝑛 is a divergence point, Lemma 7 showed that there is a decision transition 𝑡′ of 𝑡𝑛 whose
firing leads to a marking 𝑚′ in which only 𝑡𝑛+1 is enabled. After 𝑡𝑛 fires, resulting in the marking
𝑚, only 𝑡′ is enabled in 𝑚. For the enabledness of 𝑡′ , we consider the following places in its preset
in the marking 𝑚: 1) 𝑝𝑑𝑒𝑐𝑖𝑠𝑖𝑜𝑛
𝑛 , which is the decision place of 𝑡𝑛 introduced by Algorithm 3 on
𝑎𝑐𝑡𝑖𝑣𝑒
Line 16, 2) 𝑝𝐶𝑠 (𝑡) , the place indicating that the sequence 𝐶𝑠 (𝑡) that 𝑡𝑛 belongs to is active.
Proof sketch. Line 17 ensures that 𝑝𝑑𝑒𝑐𝑖𝑠𝑖𝑜𝑛
𝑛 is in the postset of 𝑡𝑛 . Therefore, there is a token
in 𝑝𝑑𝑒𝑐𝑖𝑠𝑖𝑜𝑛
𝑛 in the marking 𝑚. Because of Line 21, 𝑝𝑑𝑒𝑐𝑖𝑠𝑖𝑜𝑛
𝑛 is in both the preset and postset
′
of 𝑡 . Knowing that 𝑡 is guaranteed to be the last activation transition that has fired, and that
the final transition of 𝐶𝑠 (𝑡) has not fired yet, Line 21 ensures that decision transitions for
non-final transitions do not consume a token from 𝑝𝑎𝑐𝑡𝑖𝑣𝑒 𝐶𝑠 (𝑡) , therefore is a token in the place
𝑝𝑎𝑐𝑡𝑖𝑣𝑒 ′ ′′
𝐶𝑠 (𝑡) . Therefore 𝑡 is enabled in 𝑚. Line 21 also ensures that any other decision transition 𝑡
with 𝑝𝑑𝑒𝑐𝑖𝑠𝑖𝑜𝑛
𝑛 in its preset will have a different active place 𝑠𝑎𝑐𝑡𝑖𝑣𝑒 in its preset. Knowing that
any activation transition other than 𝑡 could not have been the last activation transition to fire,
36
�Bart-Jan Hilbrands et al. CEUR Workshop Proceedings 21–39
there can be no token in 𝑠𝑎𝑐𝑡𝑖𝑣𝑒 . Therefore, any transition 𝑡′′ cannot be enabled in 𝑚. Therefore,
only 𝑡′ is enabled in 𝑚.
Theorem 1. A component always satisfies a set of diverging, single-stage causal sequence con-
straints after applying Sequence Algorithm 2
Proof sketch. To show that 𝒪 satisfies an arbitrary causal sequence constraint after applying
Sequence Algorithm 2, it needs to be shown that the property introduced in Definition 3
holds. That is, it must be shown that there is exactly one possible firing sequence, excluding
transitions introduced by the Sequence Algorithm, after any 𝑡 fires until the last transition of
𝐶𝑠 (𝑡) fires. Following Lemma 5, any transition not belonging to a sequence is disabled after 𝑡
fires. Furthermore, any transition belonging to a sequence that is not 𝑡0 is disabled following
Lemma 4. Because 𝑡0 is guaranteed to be enabled following Lemma 3, the only possible transition
that be enabled after 𝑡 fires is 𝑡0 . Following Lemmas 6, 7 and 8, the 𝑛th sequence transition
to fire after 𝑡 fires, must be the 𝑛th element of 𝐶𝑠 (𝑡), as any transition not belonging to a
sequence is disabled, and any transition 𝑡𝑛 belonging to a sequence can only be enabled after
𝑡
𝑡𝑛−1 fires. Therefore, for any marking 𝑚′ , if 𝑚′ −→, when excluding any transitions introduced
by Sequence Algorithm 2, there exists exactly one firing sequence from 𝑚′ that is 𝐶𝑠 (𝑡).
6. Conclusions
This paper addressed the challenge of correctly and cost-effectly designing complex component-
based systems, built from reusable components that provide and consume services to and from
each other over a set of interfaces. The state of an interface on a component may be dependent
on the state of another, which may result in deadlock, livelock, or unbounded behavior. To
address this challenge, the paper proposed a way to capture partial specifications of component
behavior as sets of commonly occurring functional constraints. We formalized such functional
constraints and presented algorithms to generate Petri nets satisfying the constraints, supported
by proof sketches to show their correctness. The approach was demonstrated through a running
example of a vending machine.
Future work involves adding support for the complete ComMA language, as the current
solution does not cover required interfaces and compound transitions. Other possible directions
include adding support for more types of functional constraints, extensions with data, and take
into account commonly occurring middleware patterns, such as blocking calls. Furthermore, a
comparison could be made between multiple encoding methods. For example, a compositional
approach using label based synchronization could be considered as an alternative approach,
making for a more modular solution that is easier to extend.
References
[1] HTSM Systems Engineering Roadmap, 2020. URL: https://hollandhightech.nl/_asset/
_public / Innovatie / Technologieen / z_pdf_roadmaps / Roadmap - Systems - Engineering -
update-2020-final-v20200724.pdf.
37
�Bart-Jan Hilbrands et al. CEUR Workshop Proceedings 21–39
[2] C. Y. Baldwin, K. B. Clark, Modularity in the design of complex engineering systems, in:
Complex engineered systems, Springer, 2006, pp. 175–205.
[3] R. N. Langlois, Modularity in technology and organization, Journal of economic behavior
& organization 49 (2002) 19–37.
[4] I. Kurtev, M. Schuts, J. Hooman, D.-J. Swagerman, Integrating interface modeling and
analysis in an industrial setting, 2017, pp. 345–352.
[5] R. van Beusekom, B. de Jonge, P. Hoogendijk, J. Nieuwenhuizen, Dezyne: Paving the way
to practical formal software engineering, Electronic Proceedings in Theoretical Computer
Science 338 (2021) 19–30.
[6] S. Bensalem, M. Bozga, J. Sifakis, T.-H. Nguyen, Compositional verification for component-
based systems and application, in: S. S. Cha, J.-Y. Choi, M. Kim, I. Lee, M. Viswanathan
(Eds.), Automated Technology for Verification and Analysis, Springer Berlin Heidelberg,
Berlin, Heidelberg, 2008, pp. 64–79.
[7] B. Metzler, H. Wehrheim, D. Wonisch, Decomposition for compositional verification, in:
S. Liu, T. Maibaum, K. Araki (Eds.), Formal Methods and Software Engineering, Springer
Berlin Heidelberg, Berlin, Heidelberg, 2008, pp. 105–125.
[8] R. van Beusekom, J. Groote, P. Hoogendijk, R. Howe, W. Wesselink, R. Wieringa,
T. Willemse, Formalising the dezyne modelling language in mcrl2, in: Critical Systems:
Formal Methods and Automated Verification, Springer, Germany, 2017, pp. 217–233.
[9] G. Engels, J. M. Küster, R. Heckel, M. Lohmann, Model-based verification and valida-
tion of properties, Electronic Notes in Theoretical Computer Science 82 (2003) 133–150.
UNIGRA’03, Uniform Approaches to Graphical Process Specification Techniques.
[10] B. Selic, Using uml for modeling complex real-time systems, in: F. Mueller, A. Bestavros
(Eds.), Languages, Compilers, and Tools for Embedded Systems, Springer Berlin Heidelberg,
Berlin, Heidelberg, 1998, pp. 250–260.
[11] C. A. R. Hoare, Communicating sequential processes, Commun. ACM 21 (1978) 666–677.
[12] D. Bera, K. Hee, van, M. Osch, van, J. Werf, van der, A component framework where port
compatibility implies weak termination, Computer science reports, Technische Universiteit
Eindhoven, 2011.
[13] D. Craig, W. Zuberek, Compatibility of software components - modeling and verification,
in: 2006 International Conference on Dependability of Computer Systems, 2006, pp. 11–18.
[14] D. Bera, K. M. van Hee, J. M. van der Werf, Designing weakly terminating ros systems,
in: S. Haddad, L. Pomello (Eds.), Application and Theory of Petri Nets, Springer Berlin
Heidelberg, Berlin, Heidelberg, 2012, pp. 328–347.
[15] I. Kurtev, J. Hooman, M. Schuts, Runtime Monitoring Based on Interface Specifications,
Springer International Publishing, Cham, 2017, pp. 335–356.
[16] J. L. Peterson, Petri nets, ACM Comput. Surv. 9 (1977) 223–252.
[17] J. Baez, J. Master, Open petri nets, Mathematical Structures in Computer Science 30 (2020)
1–28.
[18] B.-J. Hilbrands, Verification of Inter-Dependent Interfaces in Component-Based Ar-
chitectures, Master’s thesis, University of Amsterdam, Amsterdam, 2021. URL: https:
//www.akesson.nl/files/students/hilbrands-thesis.pdf.
[19] W. M. P. van der Aalst, C. Stahl, M. Westergaard, Strategies for modeling complex processes
using colored petri nets, in: K. Jensen, W. M. P. van der Aalst, G. Balbo, M. Koutny, K. Wolf
38
�Bart-Jan Hilbrands et al. CEUR Workshop Proceedings 21–39
(Eds.), Transactions on Petri Nets and Other Models of Concurrency VII, Springer Berlin
Heidelberg, Berlin, Heidelberg, 2013, pp. 6–55.
39
�