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 functionality. 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.
Systems are becoming increasingly complex, making them challenging to develop, maintain, and
evolve over time [
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 ofline test scenarios to check if the implementation conforms to the specified contracts. Furthermore, since 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.
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 deadlock, 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.
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.
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.
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 [
There are also several works [
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
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[
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 of, and may restock the machine with LoadProduct.
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
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.
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) if: ∀ ∈ : |∙ | ≤ 1 ∧ |∙ | ≤ 1 and all markings
have exactly one token [
While open Petri nets (OPNs) [
Figure 2 shows the interface skeletons of the two vending machine interfaces represented as
because the transformation does not consider functional constraints during the transformation.
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
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.
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 if for any given transition ∈ and marking ∈ ():
if →− then ∀ ∈ () : () = 1 Given constraint 1 of Figure 1c, we can then define (LoadProduct) = {Empty}.
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 if for any given transition ∈ and marking ∈ ():
if →− then ∀ ∈ () : () = 0
Given constraint 2 of Figure 1c, we can then define (Order) = {Error}.
Definition 3 (Causal sequence constraint). Given a Component and a set of transitions ⊆ , a causal sequence constraint is defined as follows:
: → * if →− ′ then: A component satisfies a causal sequence constraint if for any given transition ∈ and marking ∈ (): ∃′→−
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 Figure 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 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,
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 of with the notion of overlapping and diverging causal sequences. It is possible that a sequence of consequence transitions 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.
t1 t0’ t2 t1’ t0 s0 s1 t3 t2’
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 diferent 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 [
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 ifres, ′ may not be in a state in which +1 can be fired.
If these two enabling constraints were absent, it would be possible for SwitchOn and Reset to ifre 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 ′.
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
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.
they satisfy a set of given functional constraints. There are obviously a lot of diferent 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 diferent 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, diferent parts of Figure 4 will be highlighted and discussed to exemplify the output of the method.
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.
vending machine component. In Figure 4, we can see a bidirectional arc created between the
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.
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 [
places have the correct number of initial tokens, depending on whether has a token initially.
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 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 13 14 end 15 end end create bidirectional arc(, t)
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.
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 diferent 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 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
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
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 (). 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 15 16 17 18 else if is a divergence point then create place(, 0 tokens); create arc(, ); foreach successor ∈ , where is a successor of , and belongs to the sequence do create transition(); create arc(, ); create bidirectional arc( , ); if enabler place of successor(t) does not exist then create place(successor(t), 0 tokens); create arc(successor(t), successor(t)); 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 end
create arc(, successor(t)) end foreach sequence , where is the final transition of do create transition( ); create arc(, ); create arc(, ); create arc( , disabler) end else if is the last transition of the sequence then create arc(, disabler); create arc(, ); else if if enabler place of successor(t) does not exist then create place(successor(t), 0 tokens); create arc(successor(t), successor(t)); create arc(, successor(t))
Algorithm 3: Causal Sequence Constraints 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 ifring 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. 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 will also have a +1 is in the postset of ′, 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 ifring 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 diferent active place in its preset. Knowing that any activation transition other than could not have been the last activation transition to fire, 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 constraints after applying Sequence Algorithm 2
Proof sketch. To show that satisfies an arbitrary causal sequence constraint after applying
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 ifres. 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 ().
This paper addressed the challenge of correctly and cost-efectly designing complex componentbased 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. (Eds.), Transactions on Petri Nets and Other Models of Concurrency VII, Springer Berlin