Before a system is built in Service Oriented Computing from interacting services, it is modeled and verified with regard to different behavioral correctness criteria, among others, deadlock freedom. For this purpose, open nets as a special class of Petri nets are frequently used. In this paper, we present and compare three formalizations of when two services interact deadlock freely. We specifically highlight subtle details of existing formalizations and propose a new formalization that matches the intuition in every case.
stituents and the standard firing rule. We assume the standard notions of markings,
enabledness, firing, and reachability in Petri nets. Otherwise, see [
For i = 1; 2 let Ni = (Pi; Ti; Fi) together with the interface (Ii; Oi) be open net structures. Without loss of generality, we assume each node x shared by N1 and N2 be an interface place: Otherwise, replace x by different instances in both open net structures. N1 and N2 are partner structures iff I1 = O2 and I2 = O1. The composition of N1 with N2 is the open net structure N1 N2 =def (P1 [ P2; T1 [ T2; F1 [ F2) together with the interface (I n O; O n I), where I = I1 [ I2 and O = O1 [ O2.
Inner nodes model a service’s business functionality and interface nodes model a service’s standardized interface. The concept of partners expresses two services’ capability of proper communication. On the level of open nets, communication of two partners N1 and N2 is the firing of an interface transition of N1 or N2 in their composition N1 N2. Additionally, we distinguish situations which N1 and N2 shall reach together, i.e., target markings.
Definition 2 (open net, partners). Let N be an open net structure, let m be a marking of N with no interface place marked, and let W be a set of markings of N with no interface place marked. Then N together with m and W is an open net, with m the initial marking of N, and W the set of target markings of N.
Let N1 and N2 be two open nets with initial markings m1, m2 and target markings W1, W2, respectively. N1 and N2 are partners iff N1 and N2 are partner structures. The initial marking m of N1 N2 is defined by m =def m1 + m2, the target markings W of N1 N2 are W =def fm1 + m2 j m1 2 W1; m2 2 W2g.
We depict the interface of an open net N by drawing its interface places on a dashed rectangle which contains all inner nodes and interface transitions of N. If N has exactly one target marking m, we indicate a place p of N with w if and only if p is marked in m. See Fig. 1 for some examples. For an open net N, its inner structure inner(N) is defined by removing the interface places of N, and restrict its initial marking and target markings accordingly. 3
In the rest of this paper we assume freely chosen partners N and P. We shall
compare several deadlock notions for open nets by means of N and P being deadlock free
partners. Intuitively, deadlock free interaction is the avoidance of unwanted situations
in which further progress in relevant parts of a system is impossible. In the model of
open nets, we formulate this as follows: Whenever one relevant part, i.e., N or P, of the
system N P stops, than there is a wanted situation, i.e., a target marking, reachable
in N P, or N and P will eventually communicate again. Massuthe [
p1 t1 p2 p3 t2 t3
ω (a) N q r d q r d q1 t4 q2 q3 t5
t6 ω (b) P q r d ω (c) Q q1 t4 q2 q3
dead in N iff no transition of N is enabled in m. A dead non-target marking of N is a deadlockPM of N. P is DFPM-interacting with N (synonymous to N and P are DFPMpartners) iff no reachable marking of N P is a deadlockPM of N P. We write DFPM(N) for the set of all open nets DFPM-interacting with N, and DFPM for the set of all DFPMpartners.
For example, the open net N (Fig. 1(a)) models a service which is able to receive a query (input place q), and then either replies to the query (output place r) or denies access (output place d). Afterwards, the service can terminate in the target marking [p3]. Typically, the decision between reply or denial is made depending on data inside the received query. As we abstract from data in open nets, we model the decision’s outcome using non-determinism (interface transitions t2 and t3). The open net P (Fig. 1(b)) is DFPM-interacting with N: Whether N sends a reply or denial, P is able to receive it. Thus, the only marking of N P with no transition enabled is the target marking [p3; q3] of N P, i.e., [p3; q3] is no deadlockPM. In contrast, the open net Q (Fig. 1(c)) is not DFPM-interacting with N: There are two deadlocksPM, [p3; r; q2] and [p3; d; q2], reachable in N Q.
Massuthe’s definition provides a good first impression on how to formalize
deadlocks in open nets. However, it is not precise enough. As an example, consider the open
net R (Fig. 2(a)), which originates from Q by adding an inner loop (transition t5). R
is as malfunctioning as Q: Two markings, [p3; r; q2] and [p3; d; q2], are reachable in
N R, such that neither N nor R is in a target marking, and they will never
communicate again. Intuitively, N and R should not be deadlock free partners. Nevertheless,
R is DFPM -interacting with N, i.e., N and R are DFPM -partners. This example shows
a general drawback of Definition 3: Every open net N has at least one open net M
which is DFPM -interacting with N. M consists of an interface that is compatible with
N’s interface, and an inner loop without communication. Wolf [
each reachable marking in inner(N), a marking is reachable in inner(N) which is a target marking or which enables an interface transition of N. P is DFKW -interacting with N iff P is responsive and no reachable marking of N P is a deadlockPM of N P. N and P are DFKW -partners iff N is DFKW -interacting with P and P is DFKW -interacting with N. We write DFKW (N) for the set of all open nets DFKW -interacting with N, and DFKW for the set of all DFKW -partners.
q r d ω (a) R q1 t4 q2 t5 q3 q r d q1 t4 q2 q3 t5
t6 ω (b) S q r d q1 t4 q2 q3 t7 t5
t6 ω (c) T
Responsiveness rules out some intuitively unwanted interacting open nets with
endless loops without communication (like R in Fig. 2(a), which is not DFKW -interacting
with N), but unfortunately not all. Figure 2 depicts an example. The open net S (Fig.
2(b)) is responsive and DFKW -interacting with N. However, we would intuitively
classify the reachable marking [p3; d; q2] of N S as a deadlock: Neither N nor S is in a
target marking, and they will never communicate again. Additionally, responsiveness is
a rather strong restriction on partners. Intuitively, N and the open net T (Fig. 2(c)) are
deadlock free partners: N T has no reachable marking which enables transition t7.
Nevertheless, T is not responsive and not DFKW -interacting with N according to Def. 4.
1 Additionally, Wolf restricts Def. 4 to bounded open nets and bounded communicating partners
for decidability reasons [
In order to overcome those drawbacks, we propose a new, third definition of deadlocks and deadlock free partners. Our definition is based on the observation that a deadlock of two interacting services N and P is intuitively described from the view of one of the involved services, e.g., N, by three facts: (1) N is in an unwanted situation, (2) further progress in N P by N alone is impossible, i.e., there is a need for interaction of P with N, and (3) P will never interact with N anymore. Therefore, we propose to describe deadlocks in open nets locally, i.e., from the view of one service, rather than from a global point of view on both partners. We do so by using the target markings of only one of the involved open nets, and by considering silent markings, which capture the absence of further communication between the partners.
Definition 5 (silent marking, deadlockRM, DFRM-partners). A marking m of N P is silent in N P iff for all markings m0 of N P reachable from m holds: At most inner transitions of P are enabled in m0. A silent marking m of N P such that mjN is no target marking of N, is a deadlockRM of N P. P is DFRM-interacting with N iff no reachable marking of N P is a deadlockRM of N P. N and P are DFRM-partners iff N is DFRMinteracting with P and P is DFRM-interacting with N. We write DFRM(N) for the set of all open nets DFRM-interacting with N, and DFRM for the set of all DFRM-partners. Notice the discrimination between wanted and unwanted situations by means of N’s target markings instead of N P’s target markings like in Def. 3 and 4. Definition 5 matches our intuition in every previously mentioned example: N and P as well as N and T are DFRM-partners, whereas all other partners are not. 4
In this section, we shall compare Definitions 3, 4, and 5 in terms of the characterized deadlock free partners, and the complexity of the notions. Given an open net N, the set of open nets deadlock freely interacting with N generally differ, depending on which definition of deadlock free interaction is employed. Every open net DFKW -interacting with N is DFPM-interacting with N as well, the opposite is not true (see R and S in Fig. 2 for an example). An open net DFRM-interacting with N can be DFPM-interacting with N, DFKW -interacting with N, or neither. Consider Fig. 3(a) for an illustration of above coherences as Venn diagram.
An open net DFRM-interacting with N, which is not DFPM-interacting with N, may seem counter-intuitive for a notion of deadlock free partners. However, Def. 5 says DFRM-partners have to be mutually DFRM-interacting with each other, therefore every two DFRM-partners are DFPM-partners as well. Again, this matches our intuition. Every two DFKW -partners are DFPM-partners. The sets of all DFKW -partners and all DFRMpartners lie diagonally: There exist DFKW -partners, which are no DFRM-partners (e.g. the open nets N and S in Fig. 1(a) and 2(b)), and vice versa (e.g. the open nets N and T in Fig. 1(a) and 2(c)). Figure 3(b) depicts above coherences.
All three presented formalizations differ in how complex it is to check whether two given open nets N and P are deadlock free partners or not. Checking according to Def. 4 is more complex than according to Def. 3, as responsiveness of N and P has to be checked additionally. Checking according to Def. 5 is more complex than according S all partners
P all partners
DFRM(N) DFPM(N) (a) deadlock free interaction
DFKW DFRM DFPM (b) deadlock free partners to Def. 4, because it is more complex to check if a marking m of N P is silent than to check if m is dead. To sum up, there is a trade-off between matching our intuitive deadlock notion and the complexity of a formalization. 5
We have presented two existing formalizations of when two services interact deadlock freely, and gave an idea of their deficits in subtle situations. Our approach for overcoming these deficits is a third formalization, describing deadlocks from a local point of view rather than globally. To the best of our knowledge, this is new. Finally, we compared all three formalizations, and highlighted their differences in complexity as well as matching our intuition. Though more complex, the new formalization matches our intuition in every case.
There exists strong theory for characterizing all deadlock free partners, based on the
two existing formalizations ([