Subscribe Now Subscribe Today
Research Article
 

Soundness Analysis of T-Restricted Interorganizational Logical Workflow Nets



Wei Liu, Yuyue Du and Haichun Sun
 
Facebook Twitter Digg Reddit Linkedin StumbleUpon E-mail
ABSTRACT

Interorganizational Logical Workflow Nets (ILWN) can efficiently model cooperative systems based on Petri nets, workflow techniques and temporal logic. But soundness of arbitrary ILWNs is hard to decide. This study defines the concept of T-restricted Logical Workflow Nets (LWN) and proposes an important subclass of ILWNs composed of n T-restricted LWNs: T-restricted ILWNs. The sufficient and necessary conditions of T-restricted ILWNs preserving soundness are obtained and the rigorous analysis approach is presented based on their static net structures only. Moreover, two approaches of combining n T-restricted LWNs into one T-restricted ILWN are given. The concepts and techniques proposed in this study are illustrated with a useful example of an auto gas station system.

Services
Related Articles in ASCI
Search in Google Scholar
View Citation
Report Citation

 
  How to cite this article:

Wei Liu, Yuyue Du and Haichun Sun, 2009. Soundness Analysis of T-Restricted Interorganizational Logical Workflow Nets. Information Technology Journal, 8: 821-829.

DOI: 10.3923/itj.2009.821.829

URL: https://scialert.net/abstract/?doi=itj.2009.821.829
 

INTRODUCTION

Due to the enhancement of reliability and safety of communication networks, the number of entities and the heterogeneity of cooperative systems are unprecedented and require new approaches to model and verify their correctness and temporal properties. It is inspiring that today’s workflow management systems support business processes of complex systems via electronic networks and are widely used by organizations to coordinate the execution of various applications representing their day-to-day tasks. A workflow is a representation of a given process that consists of well-defined set of activities, referred to as tasks. Each of the tasks in the process represented by a workflow serves a given function and has some input requirements and may also generate information as a part of its output. The tasks in a workflow are usually related and dependent on one another. These task dependencies are called intra-workflow dependencies. Task dependencies may also exist across workflows where multiple organizations are involved in shared business processes, such task dependencies are referred to as inter-workflow dependencies. In general, task dependencies are divided into three types: control dependencies, value dependencies and external dependencies.

Van der Aalst (2000) defined interorganizational workflow nets (IOWF) to model loosely coupled interorganizational workflows. An IOWF-net describes the local workflows and the coordination structure for their interaction. XRL (eXchangeable Routing Language) language (Verbeek et al., 2002), which based XML language, was used for the specification of interorganizational workflows. Van der Aalst (2003) described formally the Public-To-Private (P2P) approach to construct interorganizational workflows based on a notion of inheritance. The public parts are related to each other, making up an interorganizational workflow. Each private workflow corresponds to an actual workflow as it is executed in one of the domains. The P2P approach guarantees that each private workflow is a subclass of the corresponding public part under projection inheritance. A new approach on the modeling of interorganizational workflows is presented based on nested Petri nets (Prisecaru and Jucan, 2008). It deals with loosely coupled Inter-organizational workflows: there are n local workflow processes which can behave independently, but need to interact at certain points in order to accomplish a global business goal. Soundness is introduced and proved.

An object-oriented technology is used to analyze the soundness of inter-organizational workflows (Sun and Du, 2008). It focuses on interactive messages in an inter-organizational system. Each workflow entity is packaged based on the object-oriented technologies. Each private workflow is considered as one object. The study put more attention on the whole part and interactive actions of the workflows. Some details inside one private workflow are neglected. It investigates interactive messages need to satisfy the properties in a sound inter-organizational workflow.

An Interorganizational Logical Workflow Net (ILWN) (Du et al., 2007) is presented for modeling and analyzing cooperative systems based on Logical Petri Nets (LPN), workflow techniques and temporal logic. It can model passing value indeterminacy and describe batch processing function of cooperative systems which the existing formal techniques cannot model. Through attaching logical expressions to some actions of an ILWN model, the size of the model is reduced. Thus, ILWN can mitigate efficiently the state explosion problem to some extent.

The modeling power of LPN and the equivalency between LPN and Petri Nets (PN) with inhibitor arcs (IPN) are analyzed and verified (Du and Guo, 2009). The equivalency is proved formally and a constructing algorithm of equivalent IPN from LPN is proposed based on the disjunctive normal forms of logic input/output expressions.

Soundness is an important property for ILWN. As a matter of fact, soundness can be decided; however, it is EXPSPACE hard (Van der Aalst, 2000). Thereby, soundness is discussed for an important subclass in this paper: T-restricted ILWN.

For the T-restricted ILWN, this study discusses how to compose ILWN to preserve soundness. Our results can be more expediently used by the designers of cooperative workflows in comparison with message sequence charts (Alur and Yannakakis,1999) because the method in this study can reduce the analysis complexity of ILWN consumedly. At last methods and concepts are illustrated with a useful example of an auto gas station system.

PRELIMINARIES

Here, we briefly review the notations of Petri nets, workflow nets and logical Petri nets.

A Petri net (Murata, 1989) is a four-tuple PN = (P, T, F, M0), where P is a set of places, T is a set of transitions, P∩T=φ, F⊆(PxT)∪(TxP) are the edges (flow relations) and M0: P→ N ∪{0} (N is a natural number set) is the initial marking of PN. R(MO) represents the set of all markings reachable from MO. x∈P∪T: •x={y| (y, x)∈F} and x•={y| (x, y)∈F}. For Q⊂P∪T, •Q=∪q∈Q •q and Q•=∪q∈q•.

Places are graphically drawn as circles, transitions are drawn as bars and the flow relations are drawn as directed arcs. A transition t is enabled if each place p∈Ct contains at least one token. When an enabled transition t fires, for ∀p∈Ct, one token is removed from p and for ∀p∈t•, one token is added to p. This results in a new marking M', denoted by M[t>M'.

A Petri net is strongly connected if and only if for every pair of nodes x and y, there is a path leading from x to y. It is bounded if and only if ∀p∈P, there is a natural number k such that ∀M∈R(M0): M(p)≤k.

Definition 1: PN = (P, T, F, M0) (Van der Aalst, 1999) is a workflow net (WF-net) iff:

PN has two special places: i and o. Place i is a source place: •i =φ; Place o is a sink place: o•=φ
If a transition t# is added to PN which connects place o with i (i.e. •t# ={o} and t# •={i}), the resulting PN is strongly connected

Note that i (o) is used to denote place i (o) and the marking with only one token in place i (o).

A workflow net is constructed by several basic building blocks: AND-split And-Join, OR-split and OR-join (Van der Aalst, 2000).

However, it is difficult that the passing value indeterminacy and batch processing function of cooperative systems are described in WF-nets.

Definition 2: A Logical petri net (Du et al., 2007) is a 7-tuple LPN = (P, T, F, Dt, I, O, M), where P is a set of places; T = TD∪ TI∪ TO is a set of transitions; TD is a set of delay transitions; TI is a set of logical input transitions; TO is a set of logical output transitions and P, TD, TI and TO are disjunct sets; F ⊆(Px(TD ∪ TI∪ TO))∪((TD ∪ TI ∪ TO) xP) is a set of arcs; Dt is a function such that ∀t∈TD, Dt(t) ∈R, which denotes the delay time of t; I is a mapping function such that t∈TI, I(t) is a logical input expression fI, while O is a mapping function such that ∀t∈TO, O(t) is a logical output expression fO; M is a marking function.

The LPN representations of logical input and output transitions are shown in Fig. 1a and b.

Firing rules of the transitions in LPNs are as follows:

∀t∈TD, dt(t)=τ, t is said to be enabled if ∀p∈Ct; M(p)=1; t is said to be firable if its enabled time is equal to τ and firing t results in a new marking M': ∀p∈Ct: M'(p)=M(p)-1; ∀p∈t•: M'(p)=M(p)+1
∀t∈TI, I(t)=fI, t is said to be enabled if fI|M = T, i.e., all input places of t satisfy the logical input expression fI at M; if t is enabled, it can fire and firing t generates a new marking M': ∀p∈Ct: M'(p)=0; ∀p∈t•: M'(p)=M(p)+1
∀t∈TO, O(t)=fO, t is said to be enabled if ∀p∈Ct, M(p)=1; if t is enabled, it can fire and generates a new marking M': ∀p∈Ct: M'(p)=M(p)-1; for t•, fO|M' = T

A logical input transition is enabled only if the available tokens of its all input places satisfy a given logical expression and there exists no token in its all input places after it fires.

Image for - Soundness Analysis of T-Restricted Interorganizational Logical Workflow Nets
Fig. 1: Representations of logical (a) input and (b) output transitions

The notation fI (fO) is used to denote the logical expression of a logical input (output) transition. Logical input or output transitions are represented graphically by the rectangles in which mark I or O is embedded, respectively. Figure 1 shows that task A is enabled only if p1 has at least one token and p2 or p3 has at least one token. The enabling conditions of logical output transitions are the same as ones of the transitions in classical Petri nets. The output places of a logical output transition must satisfy its logical expression fO and depends on new generated values when firing it. The output of logical output transitions is non-determinate in static structures. Figure 1b denotes that one token is generated in p1 and there is one token in one of p2 and p3, or in each of them, after executing task A.

Definition 3: Let M be a reachable marking in a LPN, α a firing sequence at M, f and g LPN formulae. α= βiΥj, βi is the prefix of α with length i and Υj is the postfix of α excluding βi, LPN formulas are defined recursively (Du et al., 2008).

|=p iff there is at least one token in place p at M
|=tfir iff transition tεT is firable at M
|=t iff transition t fires, t∈TD∪TI∪TO.
|=f∨g iff |=f or |=g
|=f∧g iff |=f and |=g
|= ¬f iff not |=f
|= f⇒g iff |=f implies |=g
|=of iff α λ and 1,Υ1>|=f
|=□f iff < Mii >|=f for every i: 0≤i≤ α
|=◊f iff ii>|=f for some i: 0≤i≤ α
|= fΔg iff if |= f and |= g then
|= f ∧ g,else |=f ∨ g

Here, symbols ¬, ∧ and ∨ are the Boolean connectives. Symbol Δ, as a substitutive operator, is used to describe the passing value indeterminacy. If f and g become true in M, then fΔg is replaced by f ∧ g and otherwise by f ∨ g. In this study, T is used to represent a logical true value in logical expressions.

T-RESTRICTED ILWN

Definition 4: (T-1-live) A transition t in a Petri net (PN, M) is 1-live iff the following holds (Van der Aalst, 1999):

For every marking M’ reachable without firing t, there is a state M’N reachable from M’ which enables t
For every marking M’ reachable via a firing sequence which fires t, there is no state reachable from M' which enables t

Definition 5: A LWN=(P, T, F, DT, I, O, M) (Du et al., 2007) is called a logical workflow net iff:

The LPN has two disjunct subsets, PC and PD and P = PC ∪ PD, where PC is a set of control places, PD a set of interface data places
PC includes two special places: i and o. Place i is a source place: •i=Ø. Place o is a sink place: o•=Ø
∀tεT, •t and t• include one control place at least, respectively
If we add a transition t# to the LPN which connects place o with i ( •t# = {o} and t# • ={i}), then its inner logical net Image for - Soundness Analysis of T-Restricted Interorganizational Logical Workflow Nets is strongly connected, where Image for - Soundness Analysis of T-Restricted Interorganizational Logical Workflow Nets= F-(PDx T∪TxPD)

There are two types of places in LWN, control places and data places. Control places are used to deposit control tokens, data places to deposit data tokens. Data places are also called interface places.

Definition 6: An LWN (Sun and Du, 2008) is sound iff in Image for - Soundness Analysis of T-Restricted Interorganizational Logical Workflow Nets

Image for - Soundness Analysis of T-Restricted Interorganizational Logical Workflow Nets there exist a firing sequence α, such that Image for - Soundness Analysis of T-Restricted Interorganizational Logical Workflow Nets
Image for - Soundness Analysis of T-Restricted Interorganizational Logical Workflow Nets there exist a firing sequence α such that Image for - Soundness Analysis of T-Restricted Interorganizational Logical Workflow Nets

In the above definition, requirement 1 means that for Image for - Soundness Analysis of T-Restricted Interorganizational Logical Workflow Nets there exists a firing sequence α such that Image for - Soundness Analysis of T-Restricted Interorganizational Logical Workflow NetsRequirement 2 means that there is no dead transition in the inner logical marking net Image for - Soundness Analysis of T-Restricted Interorganizational Logical Workflow NetsSince, the interface data places and their related arcs are omitted in an inner logical net, we can think of the marking net Image for - Soundness Analysis of T-Restricted Interorganizational Logical Workflow Nets as its logical workflow process, i.e., the corresponding organization has full control over the local part of the LWN.

We demand that each interface data place in PD has one sender and one receiver. Moreover, each transition involved in interface data places between instances has to be T-1-live. A logical workflow net which meets these two requirements is called a T-restricted logical workflow net.

Definition 7: (T-restricted logical workflow nets) A T-restricted logical workflow net is a logical workflow net which satisfies the following requirements:

p∈PD, |C p|= |p• |=1
t∈CPD∪ PD•, t is T-1-live

Definition 8: Let LWNj = (Pj, Tj, Fj,M0j, DTj, Ij,Oj) be an LWN of the j-th cooperative organization, j = 1, 2, . . .,n. ILWN = (P, T, F,M0,DT, I,O) is an ILWN iff the following hold.

P = ∪1≤j≤n Pj ; T = ∪1≤j≤n Tj ; F =∪1≤j≤n Fj
tεTj, DT(t) = DTj(t), j = 1, 2, . . .,n
tεTIj, I(t) = Ij(t) and ∀tεTOj,O(t) = Oj(t)

Where, TIj is a set of logical input transitions in Tj and Toj is a set of logical output transitions in Tj, j =1, 2, . . .,n.

M0 is the initial marking and ∀p ε Pj : M0(p) =M0j(p), j = 1, 2, . . .,n
The transition firing rules of the ILWN are the same as in Definition 3

If an additional transition t#j is added to LWNj,which connects place oj with ij, j = 1, 2, . . ., n, ILWN# = (P, T#,F#,M0,DT, I,O) is called an extended ILWN, where T# = T ∪ {t#1, . . ., t#n } and F# = F ∪ {(o1, t#1), (t#1, i1), . . ., (on, t#n ), (t#n, in)}.

Definition 9: (T-restricted ILWN) A ILWN is called T-restricted ILWN if each of its LWNs is T-restricted.

An ILWN can be obtained through superposing the interface data places among the related LWNs by the definition if the local workflow processes of each cooperative organization are modeled by an LWN. However, the correctness of an ILWN may be destroyed due to asynchronous communication since the passing values between organizations may be subjected to order errors of some sending and receiving actions or incorrect choice of firing sequences. In Fig. 2, LWN1 and LWN2 are both sound, but their ILWN is not live, because t11, t12, t21 and t22 are dead transitions. But if the order of a receiving action and a sending action is exchanged in one of two LWNs, the ILWN is live. For example, if (p2, t21) and (t22, p1) are replaced with (p2, t22) and (t21, p1), respectively, the ILWN becomes live.

Image for - Soundness Analysis of T-Restricted Interorganizational Logical Workflow Nets
Fig. 2: An ILWN composed of two LWNs

Definition 10: An ILWN is sound (Du et al., 2007) iff

Each of its LWNs is sound
ILWN# is live

Definition 11: Let LWN be a logical workflow net. C is a path leading from a node n1 to a node nk iff there is a node sequence 1,n2,…,nk> in the LWN such that (ni,ni+1)ε(TxP)∪(PxT), i = 1,2,…,k-1. Assume that & (C) denotes the alphabet of a path C, i.e., & (C) = {n1,n2,…,nk}.

Soundness analysis of ILWNs: Here, soundness of T-restricted ILWN is analyzed. In the following, this study discusses soundness of a T-restricted ILWN composed of two T-restricted LWNs. The output transition of p is denoted by s(p). The input transition of p is denoted by r(p).

Theorem 1: Let ILWN be T-restricted and composed of two sound LWNs: LWN1 and LWN2. ∀p, qεPD, s(p)εT1, s(q)εT2, c1 is an arbitrary path leading from i1 to s(p). c2 is an arbitrary path leading from i2 to s(q).Ti1 is the set of input transitions on path c1. Ti2 is the set of input transitions on path c2.ILWN is sound iff r(q) ∉ Ti1 or r(p) ∉ Ti2.

Proof
Necessity: Since LWN1 and LWN2 are sound, each of their Image for - Soundness Analysis of T-Restricted Interorganizational Logical Workflow Netsis live. If both LWNs in an ILWN are sound,the correctness of the ILWN depends on the liveness of the transitions related to the places in PD and their precedence order in every local workflow process. Based on definition of ILWN, however, the order cannot be updated when an ILWN is constructed, i.e. the structural order of the transitions in every LWN is the same as in the ILWN. Consequently, when both LWNs are sound in an ILWN, if the ILWN is not live, this means that the incorrect order of the transitions related to the interface data places in some LWNs leads to some dead ones in the ILWN.

Case 1: If t∈T∩(•PD∪PD•) is not in conditional routing structures, this means that the sending and receiving actions between LWN1 and LWN2 are only in sequential routing constructions and parallel routing constructions in LWN1 and LWN2. By means of the conditions of the theorem, p∈PD, |Cp|= |p•*=1, r(q) ∉ Ti1 or r(p) ∉ Ti2, i.e., r(q) ∈ Ti1 and r(p) ∈ Ti2 are not satisfied simultaneously. That is to say, it will not happen that s(p) ∈T1 waits to receive the data q to be not sent by LWN2 and s(q) ∈T2 waits to receive the data p to be not sent by LWN1. Thereby, each transition in c1 and c2 is live in the ILWN.

Case 2: If t∈T∩(•PD∪PD•) is in conditional routing structures, there exist two cases.

For t∈T∩CPD, if the branch that contains t is not selected, t will not fire. It is possible r(T•1PD) will not fire. Thus, r(T•1PD) is not live
For t∈T∩PD•, if the branch that contains t is not selected, t will not fire. It is possible •T⊆PD still contains one token even when one workflow finishes

However, by means of the conditions of the theorem, t∈CPD∪ PD•, t is T-1-live, i.e.,t∈CPD∪ PD• must fire once. So the above two cases will not happen. In addition, by means of the other conditions of the theorem, the analysis is similar to case 1.So t∈T∩(•PD∪PD•) in conditional routing structures is also live in the ILWN.

Sufficiency: Let ILWN be sound, but r(q) ∉ Ti1 ∨ r(p) ∉ Ti2=.F., i.e., r(q)∈Ti1∧ r(p)∈Ti2.This means that s(p) ε T1 waits to receive the data q to be not sent by LWN2 and s(q)εT2 waits to receive the data p to be not sent by LWN1.This causes a deadlock. ILWN is not sound. This conclusion conflicts with conditions. So, the assumption is false, i.e., r(q) ∉ Ti1 or r(p) ∉ Ti2.

Corollary 1: An ILWN composed of n LWNs (LWN1, LWN2, ….. LWNn ) is sound if and only if:

LWNi, LWNj(1i and LPNj is sound
ILWN composed of ILWN' and other n-2 LWNs (LWNm1, LWNm2, ….. LWNm(n-2). mk≠ i and mk≠ j) is sound

Proof: It is similar to the Theorem 1. Based on Theorem 1,it is easy to verify the corollary 1.

Corollary 2: An ILWN composed of n LWNs (LWN1, LWN2, ….. LWNn ) is sound if and only if:

LWNi, LWNj(1i and LWNj is sound
For every two LWNs :LWNi, LWNj, an ILWNm is obtained through the combination of them. Thus, n/2 ILWNs are gotten. The ILWN composed of these n/2 ILWNs is sound

Proof: It is similar to the Theorem 1.Based on Theorem 1, it is easy to verify the corollary 2.

THE EXAMPLE OF AN AUTO GAS STATION SYSTEM

An auto gas station example is modeled and analyzed to illustrate concepts and techniques proposed in this study. It is designed based on an auto gas station example (Corbett, 1996). The model is as follows:

Image for - Soundness Analysis of T-Restricted Interorganizational Logical Workflow Nets

An auto gas station system is made up of three parts: a customer, an operator and a pump. In the example, an operator first accepts a customer’s prepaid and then accepts charge of pump.

The workflow model of a customer is described by Fig. 3. The workflow model of an operator is shown in Fig. 4. The workflow model of a pump is shown by Fig. 5. In Fig. 3, some logical input expressions and logical output expressions must be satisfied: fo(t3) = wait -ack-o-4∧ack-entry-o-4,fI(t4)=ack-accept-o-4∧ wait- ack-o-4, fo(t5)=wait-ack-p-5∧ack-entry-p-5, fI(t6)=ack -accept-p-5∧ wait-ack-p-5, fo(t7)=wait- ack-p-6∧ack- entry-p-6, fI(t8)=ack-accept-p-6∧ wait- ack-p-6∧ack -entry-c-29, fo(t9)=end-loop-8∧ack-accept-c-29. In Fig. 4, some logical input expressions and logical output expressions must be satisfied: fI(t23)=select-23 ∧ack-entry-o-4,fo(t24)=ack-entry-p-25∧wait-ack-p-25, fI(t25)=wait-ack-p-25∧ack-accept-p-25, fo(t26)=ack- accept-o-4∧end-select-31, fI(t28)=select-23∧ack-entry-o-16,fo(t29)=ack-entry-c-29∧wait-ack-c-29,fI(t30)= end-accept-30∧ack-accept-c-29. In Fig. 4, some logical input expressions and logical output expressions must be satisfied: fI(t13)=accept-13∧ack-entry-p-25,fo(t13')= ack-accept-p-25∧accept-14,fI(t14)=ack-entry-p-5∧accept-14,fo(t14')=ack-accept-p-5∧ accep-15,fI(t15)=accep-15∧ack-entry-p-6,f0(t16)=ack-entry-o-16∧wait-ack-o-16,fI(t17)= wait-ack-o-16∧ack-accept-o-16,f0(t18)=ack-accept-p-6∧end-loop-18.

Image for - Soundness Analysis of T-Restricted Interorganizational Logical Workflow Nets
Fig. 3: The LWN model of a customer

Image for - Soundness Analysis of T-Restricted Interorganizational Logical Workflow Nets
Fig. 4: The LWN model of an operator

According to Definition 7, we can judge that three logical workflow nets in Fig. 3-5 are sound. In the following, how to combine the three LWNs into one ILWN and how to verify the soundness of the ILWN are illustrated.


Image for - Soundness Analysis of T-Restricted Interorganizational Logical Workflow Nets
Fig. 5: The LWN model of a pump

Based on Corollary 1, firstly, the LWN of an operator and the LWN of a pump may be combined into one ILWN and the soundness of the ILWN can be verified by Theorem 1. Second, the LWN of an customer and the ILWN of an operator and an pump may be combined into one new ILWN and the soundness of the newly combined ILWN can be verified by Theorem 1:

(1)
Combine the LWN of an operator and the LWN of a pump into one ILWN. There are four interface data places between the LWN of an operator and the LWN of a pump: let PD={ack-entry-p-25,ack-accept-o-16,ack-accept-p-25,ack-entry-o-16}. s(ack-entry-p-25)=t24∈T(operator),s(ack-accept-o-16)=t31∈T(operator),s(ack-accept-p-25)=t13'∈T(pump),s(ack-entry-o-16)=t16∈T(pump).r(ack-entry-p-25)=t13∈T(pump),r(ack-accept-o-16)=t17∈T(pump),r(ack-accept-p-25)=t25∈T(operator),r(ack- entry-o-16)=t28∈T(operator). there is one path co1 from begin-21-operator to s(ack-entry-p-25)=t24.co1:begin-21-operator→t20→loop-22→t21→select-23 →t23→ entry-p-25→t24.

There are four paths from begin-21-operator to s(ack-accept-o-16)= t31∈T(operator).co2:begin-21-operator→t20→loop-22→t21→select-23→t23→entry-p-25→t24→wait-ack-p-25→t25→end-accept-26→t26→end-select-31→t32→end- loop-32→loop-32→t21→select-23→t28→entry-c-29→t29→wait-ack-c-29→t30→ end-accept-30→t31.co3:begin-21-operator→t20→loop-22→t21→select-23→t23→ entry-ex-24-4→t26→end-select-31→t32→end-loop-32→loop-32→t21→select-23→t28→entry-c-29→t29→wait-ack-c-29→t30→end-accept-30→t31.co4:begin-21-operator→t20-loop-22→t21→select-23→t23→entry-p-25→t24→wait-ack-p- 32→loop-32→t21→select-23→t28→entry-ex-28-16→t31.co5:begin-21-operator→t20→loop-22→t21→select- 23→t23→entry-ex-24-4→t26→end-select-31→t32→end-loop-32→loop-32→t21→select-23→t28→entry-ex-28-16→t31.

There is one path from begin-11-pump to s(ack -ent ry -o-16)=t13'∈T(pump).cp1: begin-11-pump →t11 → loop-12→t12→accept-13→t13→accept-14'→t13'.

There is one path from begin-11-pump to s(ack- entry-o-16)=t16∈T(pump).cp2: begin-11-pump→t11→loop-12→t12→accept-13→t13→accept-14'→t13'→accept-14→t14→accept-15'→t14'→accept-15→t15→entry-o-16→t16.

To1 denotes the set of transitions receiving interface data places of & (co1). To1=ø.To2 denotes the set of transitions receiving interface data places of & (co2). To2={t25,t28}.To3 denotes the set of transitions receiving interface data places of & (co3). To3={t28}.To4 denotes the set of transitions receiving interface data places of & (co4). To4={t25,t28}.To5 denotes the set of transitions receiving interface data places of & (co5). To5={t28}.Tp1 denotes the set of transitions receiving interface data places of & (cp1). Tp1={t13}.Tp2 denotes the set of transitions receiving interface data places of & (cp2). Tp2={t13}.

r(ack-accept-p-25)=t25∈T(operator)∉To1,r(ack-accept-p-25) = t25∈T(operator) ∈To2, r(ack-accept-p-25)=t25∈T(operator)∉To3,r(ack-accept-p-25)=t25∈T(operator) ∈To4, r(ack-accept-p-25) = t25∈T(operator) ∈To5, r(ack-entry-o-16)=t28∈T(operator)∉To1, r(ack- entry -o-16)=t28∈T(operator) ∈To2, r(ack-entry-o-16) = t28 ∈T(operator) ∈To3, r(ack-entry-o-16) = t28∈ T(operator) ∈To4, r(ack-entry-o-16) = t28∈T(operator) ∈To5, r(ack-entry-p-25) = t13∈T(pump)∈Tp1,r(ack-entry- p- 25) = t13∈T(pump)∈Tp2 r(ack-accept-o-16) = t17∈T(pump)∉Tp1,r(ack-accept-o-16) = t17∈T(pump)∉Tp2.

Image for - Soundness Analysis of T-Restricted Interorganizational Logical Workflow Nets
Fig. 6: The ILWN composed of an operator and a pump

For ack-entry-p-25∈PD, ack-accept-p-26∈PD, s (ack-entry-p-25) = t24∈T (operator), s(ack-accept-p-25) = t13' ∈T(pump),r(ack-entry-p-25)=t13∈T(pump)∈Tp1,r(ack-accept-p-25)=t25∈T(operator)∉T01.

In the same way, we can include for s (ack-entry-p- 25) = t24∈T(operator), s(ack-entry-o-16) = t16∈T(pump). r(ack-entry-p-25) = t13∈T(pump)∈Tp2, r(ack-entry-o-16)= t28∈T(operator)∉T01.

For s(ack-accept-o-16) = t31∈T(operator),s(ack- accept-p-25) = t13'∈T(pump). r(ack-accept-o-10) = t17∈ T(p ump)∈Tp2,r(ack-accept-p-25) = t25∈T(operator)∉T01, r(ack-accept-o-10) = t17∈T(pump)∉Tp1,r(ack-entry-p-25) = t25∈T(operator)∈T0i = .T. i∈{2,3,4,5}.

For s(ack-accept-o-16) = t31∈T(operator),s(ack-entry-o-16) = t16∈T(pump). r(ack-accept-o-10) = t17∈T(pum p)∈Tp2,r(ack-entry-o-16) = t28∈T(operator)∉T01, r(ack-accept-o-10) = t17∈T(pump)∉Tp1,r(ack-entry-o-16) = t28∈T(operator)∈T0i = .T. i∈{2,3,4,5}.

Thereby, the conditions of Theorem 1 are satisfied. According to Theorem 1, the soundness of the ILWN composed of an operator and a pump can be verified. The ILWN composed of an operator and a pump is shown in Fig. 6.

Image for - Soundness Analysis of T-Restricted Interorganizational Logical Workflow Nets
Fig. 7: The ILWN composed of a customer,an operator and a pump

(2)
In the same way, combine the ILWN of a customer and the ILWN composed of an operator and a pump into one new ILWN. There are eight interface data places between the LWN of a customer and the ILWN composed of an operator and an pump: let PD={ack-entry-o-4, ack-accept-o-4, ack-entry-p-5, ack-accept-p-5, ack-entry-p-6, ack-accept-p-6, ack-entry-c-29, ack-accept-c-29}.Based on Theorem 1, soundness of the ILWN can also be verified. The ILWN composed of a customer, an operator and a pump is shown in Fig. 7

So, according 1 and 2, it can be included that the ILWN composed of an operator, a pump and a customer is sound.

CONCLUSION

In this study, soundness of T-restricted ILWN is analyzed. A simple analysis approach is given and the inheritable conditions of soundness are obtained. Theorem 1 shows that an ILWN composed of two LWNs will preserve soundness if some conditions are satisfied.

Table 1: Symbols and abbreviations
Image for - Soundness Analysis of T-Restricted Interorganizational Logical Workflow Nets

Corollary 1 and corollary 2 give the constructing algorithm of ILWN composed of n LWNs to ensure soundness. The use of the methods and techniques is demonstrated by analyzing the example of an auto gas station system.

Further research work is to study synthesis and property-preservation of other subclasses of ILWN and LPN.

For clarity of symbols, some symbols and abbreviations are listed in Table 1.

ACKNOWLEDGMENTS

This research is supported in part by the National Natural Science Foundation of China under Grants 60773034, 90818023, 90718012 and 60803032; the Taishan Scholar Construction Project of Shandong Province, China; the Scientific and Technological Developing Program of Shandong Province of China under Grant 2008GG30001024 and the Open Project of the State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences under Grant SYSKF0804; the Research Project of SUST Spring Bud in Shandong University of Science and Technology in 2009 and the Graduate Innovation Fund of Shandong University of Science and Technology.

REFERENCES

1:  Alur, R. and M. Yannakakis, 1999. Model checking of message sequence charts. Software Concepts Tools, 17: 70-77.

2:  Corbett, J.C., 1996. Evaluating deadlock detection methods for concurrency software. IEEE Trans. Software Eng., 22: 161-180.
CrossRef  |  Direct Link  |  

3:  Du, Y.Y., C.J. Jiang and M.C. Zhou, 2007. Modeling and analysis of real-time cooperative systems using petri nets. IEEE Trans. Syst. Man Cybern. Part A: Part A: Syst. Hum., 37: 643-654.
CrossRef  |  Direct Link  |  

4:  Du, Y.Y., C.J. Jiang and M.C. Zhou, 2008. A petri-net-based correctness analysis of internet stock trading systems. IEEE Trans. Syst. Man Cybern. Part C: Appl. Rev., 38: 93-99.
CrossRef  |  Direct Link  |  

5:  Du, Y.Y. and B.Q. Guo, 2009. Logic petri nets and equivalency. Inform. Technol. J., 8: 95-100.
CrossRef  |  Direct Link  |  

6:  Murata, T., 1989. Petri nets: Properties, analysis and applications. Proc. IEEE., 77: 541-580.
CrossRef  |  Direct Link  |  

7:  Prisecaru, O. and T. Jucan 2008. Interorganizational workflow nets: A petri net based approach for modelling and analyzing interorganizational workflows. Proceedings of the 4th International Workshop on Enterprise and Organizational Modeling and Simulation held in conjunction with the CAiSE'08 Conference, June 16-17, 2008, Montpellier, France, pp: 64-78
Direct Link  |  

8:  Sun, H.C. and Y.Y. Du, 2008. Soundness analysis of inter-organizational workflows. Inform. Technol. J., 7: 1194-1199.
CrossRef  |  Direct Link  |  

9:  Van der Aalst W.M.P., 1999. Interorganizational workflows: An approach based on message sequence charts and Petri nets. Systems analysis-Modelling-Simulation, 35: 345-357.

10:  Van der Aalst, W.M.P., 2000. Loosely coupled interorganizational workflows: Modeling and analyzing workflows crossing organizational boundaries. Inform. Manage., 37: 67-75.
CrossRef  |  Direct Link  |  

11:  Van der Aalst, W.M.P., 2003. Inheritance of interorganizational workflows: How to agree to disagree without loosing control?. Inform.Technol. Manage., 4: 345-389.
CrossRef  |  Direct Link  |  

12:  Verbeek, H.M.W., A. Hirnschall and W.M. P. van der Aalst, 2002. XRL/Flower: Supporting inter-organizational workflows using xml/petri-net technology. Proceedings of the Web Services, E-Business and the Semantic Web, May 27-28, 2002, Toronto, Canada, pp: 93-108
Direct Link  |  

©  2022 Science Alert. All Rights Reserved