On quantitative Analysis of Time Open Workflow Nets and Parametric Extension Zohra Sbaï Kamel Barkaoui Université de Tunis El Manar Laboratoire CEDRIC Ecole Nationale d’Ingénieurs de Tunis Conservatoire National des Arts et Métiers BP. 37 Le Belvédère 292 rue Saint Martin 1002 Tunis, Tunisia Paris Cedex 03, France zohra.sbai@enit.rnu.tn kamel.barkaoui@cnam.fr Collaborative systems design is today a complex process especially where constraints such as tasks delays or resources handling have to be considered. In addition to a well constructed model of a workflow system, a prior and rigorous verification phase is important to ensure a correct execution of the system. In this direction, we are interested in this paper by the modeling and the analysis of interacting processes in particular those constrained by timing delays. First, we present the Time open Workflow nets (ToWF-nets) which stand for a sub-class of Petri nets dedicated to model any business process which interact with other partners via interface places in order to meet a common goal. Then, after recalling the semantics of ToWF- nets, we investigate in presenting our recent results in quantitative verification of properties related to the correct communication of various ToWF-nets. We show how to make a TCTL based model checking of the studied properties. Finally, we extend our analysis approach of ToWF-nets to cover concurrent processes leading thus to propose a parametric verification of ToWF-nets. Time Open Workflow Nets, Collaborative Systems, Quantitative Analysis, Timed Computational Tree Logic, Parametric Verification 1. INTRODUCTION and that’s why it is very studied in academic as well as industrial environment. Nowadays, collaboration in organizations is more and more sought since it allows to end users to In collaborative systems in general, different part- benefit from more enhanced and complex services. ners, having their own processes, interact together Although it is possible to allow complex services in order to achieve a common goal. We focus in this with a single organization, it is almost impossible to paper on the modeling and the analysis of such sys- provide, in this case, simple services nor to reuse tems involving multiple communicating processes. In them. So, it is important to provide simple services the modeling phase, we propose to use Time Open and to allow their composition, if necessary, for Workflow Nets (ToWF-nets), a sub class of Time more complex tasks. For instance, manufacturing Petri Nets (TPN) to model workflow processes with systems can be seen as a network of servers and timing delays and with ability to communicate with queues. This system process can be seen as a partners. A ToWF-net consists of an open workflow composition of multiple services interacting together net (oWF-net) in which we associate with each to fulfill a unique goal. As an example, we mention transition a minimum and a maximum amount of time a factory which make shirts. The first stage in needed to its execution. An oWF-net is a workflow shirt manufacturing is the cutting of the material to net augmented with special places called interface different shapes. Then, the next stage is to sew places and used to interact with other processes. the pieces together. Finally buttons and a quick iron are added. This composition is more and more For the purpose of analysis, we propose to enhance studied when treating inter organizational processes. a formal verification due to solid theoretical basis We mention for example a manufacturing enterprize of formal methods. More precisely, we adopt an which has to communicate with clients, suppliers, analysis method based on the well known model etc. in order to fulfill the manufacturing task. Thus checking techniques. In fact, Model checking is an the notion of services composition is of great need automated verification technique for proving that a model satisfies a set of properties specified in • temporal logic. Given a concurrent system Σ and As mentioned above, oWF-nets nets are mainly a temporal logic formula ϕ, the model checking the extension of workflow nets (WF-nets) to problem is to decide whether Σ satisfies ϕ. Hence, model workflow processes which interact with other we have to formulate in temporal logic the properties processes via interface places. Simple WF-nets to be verified. This kind of verification is situated (Sbaï and Barkaoui (2013, 2012)) is a result of at the design phase, allowing thus to find bugs as Petri nets’ application to workflow management. The early as possible and therefore to reduce the cost of choice of Petri nets is explained by the fact that they failures. This, especially, permits us to check as early form a powerful formalism expressing the control as possible if two or more processes are compatible flow in business processes (van der Aalst (1996); before their composition. We express the proposed Esparza et al. (1989); Ellis et al. (1995); De Michelis properties in Timed Computation Tree Logic (TCTL). et al. (1994)). The rest of the paper is organized as follows. Commonly, a Petri net is a 4-tuple N = (P, T, F, W ) Section 2 is dedicated to the presentation of ToWF- where P and T are two finite non-empty sets of nets for modeling interacting processes which are places and transitions respectively, P ∩ T = ∅ , constrained by timing delays. In this section, we F ⊆ (P × T ) ∪ (T × P ) is the flow relation, and present the semantics of the model in terms of states W : (P × T ) ∪ (T × P ) → N is the weight function and the states evolution. In section 3, we highlight of N satisfying W (x, y) = 0 ⇔ (x, y) ∈ / F . If quantitative analysis results of ToWF-nets. We recall W (u) = 1 ∀u ∈ F then N is called an ordinary net first the principle of TPN-TCTL temporal logic, then and it is denoted by N = (P, T, F ). For every node we characterize some properties of interest and x ∈ P ∪ T , the set of input nodes of x is defined by • express them in this temporal logic and finally, x = {y|(y, x) ∈ F } and the output nodes of x form we detail how to model check these properties a set denoted by x• = {y|(x, y) ∈ F }. We refer the via several examples. We focus in section 4 on reader to (Barkaoui et al. (2007)), for more Petri nets a parametric verification of ToWF-nets composition notations used in this paper. and on some experiments in Romeo model checker. Finally, section 5 presents related work and section A Petri net which models a workflow process is called 6 concludes the paper with a discussion and a a WF-net (van der Aalst (1997)). An ordinary Petri proposition of future work. net N = (P, T, F ) is a WF-net iff N has one source place i named initial place (containing initially one token) and a sink place f named final place. In 2. TIME OPEN WORKFLOW NETS addition to this characteristic, every node in a WF- This section is dedicated to present Time open net n ∈ P ∪ T exists in a path from i to f . Workflow nets (ToWF-nets) : a Petri nets sub class For processes composition, we propose to model allowing to model workflow processes communicat- each process by a WF-net describing the tasks ing with partners via interface places. After defining to be performed as well as their routing. Then, ToWF-nets model and semantics, we expose some the conversation between the involved processes results on reachability analysis. is ensured by the communication places used for 2.1. ToWF-nets to model communicating the conversation and/or the messages sending. processes Thus, we are using open WF-nets (oWF-nets) which extend the classical WF-nets by integrating interface To model a composition of interacting processes, places to ensure asynchronous communication with we refer to Petri nets due to their expressive the different partners. Hence, a composition is power as well as their theoretical basis. The well modeled by a set of oWF-nets interacting via known Petri net class used in this modeling is interface places. Note that these places are used to named open workflow nets (oWF-nets) (Karsten and connect only transitions from different processes. Schmidt (2005); Sbaï and Barkaoui (2013); Martens (2005); Massuthe et al. (2005)). Each involved Now when we focus on incorporating time con- process is modeled by an oWF-net possessing straints, we find different proposals which are based interface places which serve for the communication on extensions of Petri nets. In general, the time con- with other processes. In this way, the interaction straints are modeled either by durations or delays. and conversation between the different processes When they are specified by durations (constants), are guaranteed. The interaction considered here is the extension associated is said to be Timed Petri ensured through operational and control behaviors. nets. These constant durations are either attached The operational behavior is specific to each process to places (the subclass is known as P-Timed Petri according to its business logic and the control nets) or to transitions (T-Timed Petri nets). In case behavior is ensured by the general behavior of any of delays adoption, the constraints are specified by partner in the composite process. means of intervals specifying the minimum and the • maximum amounts of time representing the transi- • F ⊆ ((P ∪ I) × T ) ∪ (T × (P ∪ O)) is the flow tions firing delays, the associated extension is called relation, Time Petri nets. These intervals are attached to places (P-Time Petri nets), transitions (T-Time Petri • F I : T → Q+ × Q+ ∪ {∞} is the function which nets) or arcs (A-Time Petri nets) leading thus to associates to each transition t ∈ T a static firing different extensions with variant semantics. interval, i.e. F I(t) = [minF I(t), maxF I(t)] where minF I(t) and maxF I(t) are rational In the case of workflow processes, several studies numbers representing the minimal and the (van der Aalst (1993); Atluri and Huang (1996); maximal firing time respectively, Ling and Schmidt (2000); MarteGou et al. (2001)) have shown the importance of temporal reasoning The marking of N is a vector of NP such that for in the specification of workflow systems. In (Ling each place p ∈ P , M (p) is the number of tokens in and Schmidt (2000)), the authors extend the simple p. The initial marking of N is Mi knowing that Mp is WF-net presented by van der Aalst (van der Aalst used to denote a marking for which M (p) = 1 and (1997)) by associating with each transition a time M (q) = 0 ∀q ∈ (P ∪ I ∪ O) \ {p}. amount representing the task duration. A temporal extension of the WF-net, called Timed WF-net is A transition t is enabled in a marking M if the proposed. The semantic adopted here is that each required tokens are present in the input places of t. enabled transition must fire immediately, otherwise We denote by En(M ) the set of all the transitions the transition will be disabled. In case of firing, its enabled in the marking M . A transition t is said duration should be respected, i.e. this transition can disabled by the firing of t0 in M if it is enabled in not be delayed. Although this approach is simple, it is M but it isn’t in M − • t0 . When focusing of newly strict in the sense that it requires fixed durations. To enabled transitions after firing a transition t from M deal with this limitation, Time Workflow nets (TWF- and leading to M 0 , we denote by N En(M, t) the set nets) are proposed allowing to associate time delays of transitions enabled after this firing. with the activities by incorporating to each transition N En(M, t) = {t0 ∈ En(M 0 )|t0 = t ∨ ¬M ≥• t +• t0 }. a time interval specifying its firing delay (Boucheneb and Barkaoui (2012); Camerzan (2007); Ling and When a transition t becomes enabled, its firing Schmidt (2000)). interval is set to its static firing interval F I(t). The upper and lower bounds of F I(t) decrease Since this time consideration is flexible and given synchronously with time, until t is fired or disabled that we are interested by modeling the composition by another firing. t can fire, if the lower bound of its of workflow processes with time constraints, we firing interval reaches 0, but when upper bound of its propose the Time open Workflow Net model (ToWF- firing interval reaches 0, t must be fired without any net) (Sbaï et al. (2014)). This model associates additional delay (strong semantic). The firing takes to each transition a static time interval which refers no time but may lead to another marking. to the execution time or delay of the corresponding activity. The formal definition of a ToWF-net model is Let us define first the state of a ToWF-net and then the following: the transition relation. Definition 1 (ToWF-net) Definition 2 A state in a ToWF-net is the state of the process that is modeled with ToWF-net after the A Time open Workflow net N is a tuple occurrence of an event. Formally, we characterize a (P, T, F, F I, I, O) with: state in a ToWF-net by a pair (M, Int) where: • P is a set of places, • M is a marking, • T is a set of transitions, • Int is a firing interval function, Int : En(M ) → • I is a set of places which represent input Q+ × Q+ ∪ {∞}. We denote Int(t) = interfaces that are responsible of messages [minInt(t), maxInt(t)]. receiving from other processes: • I = ∅. The initial state of a ToWF-net is (M0 , Int0 ) where • O is a set of places which represent output M0 = Mi (since in a ToWF-net, only i contains interfaces responsible of messages sending to initially one token) and Int0 (t) = F I(t) ∀t ∈ En(M0 ). other partners: O• = ∅. Starting from the initial state (M0 , Int0 ), the net • I, O and P are disjoint. I and O connect evolves following the occurrence of events. An event transitions of different processes. corresponds to either a transition firing or a time progression. Hence, we define the transition relation • between states s1 = (M1 , Int1 ) and s2 = (M2 , Int2 ) of Petri nets as well as timed automata) is d t based in general on abstraction, which preserves by → in case of time progression and by → in case of a firing. We explicit in the following the conditions reachability properties. Such an abstraction for of state evolution and how to compute the resulting timed models, consists in considering only one state after an event occurrence. node for all states reachable from the same firing sequence while abstracting from their firing times. t 1. s1 → s2 if and only if s2 is immediately reachable The grouped states, known as state classes, are from s1 by firing the transition t, i.e. then considered modulo some equivalence relation t ∈ En(M1 ) and minInt1 (t) = 0, preserving properties of interest. M2 = M1 −• t + t• , and In return, the state class method is intended to ∀t0 ∈ En(M2 ), Int2 (t0 ) = provide a finite representation of the infinite state 0 0  F I(t ) if t ∈ N En(M1 , t) space of any bounded time Petri net. Int1 (t0 ) otherwise Technical classes produce for a large class of time d 2. s1 → s2 ∀d ∈ R if and only if state s2 is reachable nets a finite representation of their behavior states, from s1 by a time progression with d time units, which allows a reachability analysis similar to that i.e. permitted for Petri nets by the technique of marking graph. minInt1 (t) + d ≤ maxF I(t), M2 = M1 , and The state classes can be represented by a marking ∀t ∈ En(M1 ), Int2 (t) = [M ax(0, minInt1 (t) − and a firing domain. Formally, a state class is a d), maxInt1 (t) − d] couple (M, D) where M is a marking and D is characterized by a set of atomic constraints over the We can now define the semantics of a ToWF-net N firing delays of enabled transitions: minF I(t) ≤ t ≤ by a transition system (S, s0 , →) with S the set of all maxF I(t) ∀t ∈ En(M ). the reachable states from the initial state s0 by → the transition relation defined above. Note that the initial class coincides with the initial state of the network. This initial class is (M0 , D0 ) We present in the following subsection some results where M0 = Mi and D0 corresponds to the firing of reachability analysis of ToWF-nets composition. domains of transitions enabled in M0 . 2.2. Reachability analysis of ToWF-nets All states within the same node share the same untimed information and the union of their time After the formal definition of ToWF-nets, we focus domains is represented by a set of atomic now on their reachability analysis. This analysis constraints handled efficiently by means of a is based on the efficient construction of the state Difference Bound Matrix (DBM) (Ridi et al. (2012)). space. A DBM form a system of linear inequalities which constrain single variables (v1 ...vn ) and their By analogy with the marking graph defined in the differences within limits identified by coefficients bij . context of an ordinary Petri net, we define a state This is formally expressed as: space by a graph containing all accessible states of a ToWF-net from the initial state. Therefore, to ( vi − vj ≤ bij i, j ∈ [0..n], bij ∈ Q calculate the state space of a ToWF-net, we must be able to calculate the reachable states by activating v0 = 0 the enabled transitions. In terms of behavior, this state classes group Definition 3 The state space of a ToWF-net has preserves highly the states traces, and thus the the following structure: SS = (S, →, s0 ); where S is safety properties. the set of nodes in form (M, Int) representing the The computation of the state class graph is neces- reachable states from the initial one s0 = (Mi , Int0 ) sary at this point to perform the various reachability ; → represents the transition relation which defines analysis. Among the abstractions proposed in the the evolution from one state to another. literature (Berthomieu and Diaz (1991); Berthomieu ∗ and Vernadat (2003); Yoneda and Ryuba (1998)), S = {s|s0 → s} is the set of reachable states of the ∗ we consider here the state class graph method model, and → is the reflexive and transitive closure (Berthomieu and Diaz (1991)) for its advantage, of →. over the others, which is the finiteness property The reachability analysis (Boucheneb and Barkaoui for all bounded time Petri nets (while using some (2012)) in timed models (such as time extensions approximations). • 3. QUANTITATIVE ANALYSIS OF TOWF-NETS We can use other compositional temporal operators (Alur et al. (1993)): EFI ϕ = E( true UI ϕ) The analysis of the state space is very significant to (Possibility), EGI ϕ = ¬ AF I ¬ϕ (All locations along the extent that it can reveal important characteristics an execution), AFI ϕ = A( true UI ϕ) (Locations along of the modeled system, about its structure and all executions), AGI ϕ = ¬ EF I ¬ϕ (All locations dynamic behavior. However, for a more accurate along all executions). verification, we should not be limited to this type of checking rather than other specific properties. Semantically, TCTL formulas are interpreted on Indeed, we focus in this section on the formal states and execution paths of a model M = (S, V ) verification of compatibility properties of ToWF-nets where S is a transition system and V is a valuation as an extension of our results of compatibility function that associates with each state the set of analysis while abstracting time information (Sbaï atomic propositions it satisfies. (Konur et al. (2013)) and Barkaoui (2014); Sbaï et al. (2014)). These properties focus on the correctness of the To interpret a TCTL formula on an execution path, interactions between the different partners. we introduce the notion of dense execution path. Let s ∈ S be a state of S, π(s) the set of all execution We propose to adopt model checking method to d t 0 0 d t 1 1 paths starting from s, and ρ = s0 → s1 → s2 ... an verify these properties since this method permits execution path of s. The dense path of the execution an exhaustive verification over all the possible path ρ is the mapping ρ̂ : P R+ → S defined by: executions. Given a concurrent system Σ and i i−1 ρ̂(r) = s + δ such that r = j=0 dj + δ, i ≥ 0 and a temporal logic formula ϕ, the model checking 0 ≤ δ ≤ di . problem is to decide whether Σ satisfies ϕ. Hence, we have to formulate in temporal logic the properties The formal semantics of TCTL is given by the to be verified. satisfaction relation defined as follows: 3.1. Model checking TPN-TCTL • M , s 2 f alse, Real systems often have behaviors that depend • M , s  φ iff φ ∈ V (s), on time. The ability to manipulate and model the temporal dimension of the events that take place in • M , s  ¬ϕ iff M , s 2 ϕ, the real world is fundamental in many applications. • M , s  ϕ ∧ ψ iff M , s  ϕ and M , s  ψ, These applications may involve banking, medical, or multimedia applications. The variety of applications • M , s  ∀(ϕ∪I ψ) iff ∀ρ ∈ π(s) ∃r ∈ I, M , ρ̂(r)  ψ motivate many recent studies that aim to integrate and all the features necessary to take into account the ∀0 ≤ r0 ≤ r M , ρ̂(r0 )  ϕ, time during verification. • M , s  ∃(ϕ∪I ψ) iff ∃ρ ∈ π(s) ∃r ∈ I, M , ρ̂(r)  ψ TCTL (Timed Computational Tree Logic) is a timed and extension of the temporal logic CTL. TCTL added ∀0 ≤ r0 ≤ r M , ρ̂(r0 )  ϕ, to CTL a quantitative information on the delays between actions. It is built from atomic propositions, When interval I is omitted, its value is by default logical connectors and temporal operators (U, F, G, [0, ∞[. X, etc.). The TCTL temporal logic can be used to check the properties of a time Petri net. The Time Petri net model is said to satisfy a TCTL formula ϕ iff M, s0  ϕ. The syntax of TCTL formulas is inductively defined by: The logic TCTL allows writing temporal properties with a quantification of the time. We chose this ϕ ::= false | ¬ϕ | ϕ ∧ ϕ | A(ϕ UI ϕ)| E(ϕ UI ϕ) approach because it is decidable and PSPACE- complete for bounded Petri nets (Boucheneb et al. where p denotes a proposition, ϕ denotes a formula (2009)). and I = [a, b] or [a, ∞[ with a ∈ N and b ∈ N. The authors of (Hadjidj and Boucheneb (2009)) A and E are temporal quantifiers over the set of have gone further by defining a sub-class of TCTL executions. Aϕ announces that all the executions for time Petri nets in dense time, called TPN-TCTL. from the current state satisfy the property ϕ. Eϕ They proved the decidability of model-checking states that from the current state, there exists an of TPN-TCTL on Petri nets and showed that its execution which satisfies ϕ. Finally ϕ UI ψ means complexity is PSPACE. that the property ϕ is true until ψ is true, and ψ will be true in the time interval I. • Definition 4 The temporal logic TPN-TCTL is does not suffer from any deadlock problem. There defined inductively by: is a distinction between syntactic compatibility which refer to the conformance of interfaces (number of TPN-TCTL ::= false | ϕ | ¬ϕ | ϕ ∨ ψ | ϕ ∧ ψ | ϕ ⇒ ψ | interfaces, names, input, ouptut, etc.) and semantic EϕUI ψ | AϕUI ψ compatibility which refer to the absence of deadlocks in the global system. In this paper, we focus only on | EGI ϕ | AGI ϕ | AFI ϕ | EFI ϕ | AG(φ1 ⇒ defining and verifying the semantic compatibility. AF[0,d] φ2 ). Before this, let us characterize the composite system Where ϕ and ψ ∈ TPN-TCTL, obtained by superposing a number of ToWF-nets which are supposed syntactically compatible. The I = [a, b] or [a, b[ with a ∈ N and b ∈ N ∪ {∞}. composite net N of nbX ToWF-nets N1 ... NnbX consists of all ToWF-nets sharing interface places. In φ1 and φ2 are propositions on markings. this composite net, every input interface of a TWF- ∀G(φ1 ⇒ ∀F[0,d] φ2 ) means that from the current net has to be an output interface place of another state, any occurrence of marking φ1 is followed by TWF-net of N . Trivially, N form a time Petri net with an occurrence of marking φ2 less of d units of time nbX output places andPnbX input places. The initial nbX later. marking of N is M0 = s=1 is . Romeo permits a practical implementation of the In (Bordeaux et al. (2005); Foster et al. (2004); verification of properties described in TPN-TCTL. Martens (2003)), the authors characterized the It is therefore possible to model check on the compatibility of non timed services as the absence of fly temporal quantitative properties. That’s why deadlock in the composite service. They considered we investigate in the following section the TCTL that two or more oWF-nets are compatible if they expression of the compatibility property and hence can (all) reach their final states. By analogy, we its verification in Romeo. consider that two or more ToWF-nets are compatible if they reach their final states as well as the timing Before this, let us recall the notation used by Romeo constraints are respected. to implement a TPN-TCTL property: In order to relax this definition, we propose different TPN-TCTLRomeo = E(p)U [a, b](q) | A(p)U [a, b](q) | categories of the compatibility property. EF [a, b](p) | AF [a, b](p) | EG[a, b](p) | AG[a, b](p) | EF [a, b](p) | (p) → [0, b](q). • Partial compatibility: A composite net N satisfies the partial compatibility if it is deadlock-free. where p, q: GMEC; U : until; E: exists; A: forall; F : • Total Compatibility: A composite net N is totally eventually; G: always; →: response; a: integer; b compatible if it is deadlock-free and furthermore, integer or inf (to denote ∞). the overall process terminates properly. GM EC = a∗M (i){+, −}b∗M (j){<, <=, >, >=, =}k • Perfect compatibility: A composite net N is | deadlock | bounded(k) | p and q | p or q | p ⇒ q | perfectly compatible if it is totally compatible and not p. the deadline constraints are satisfied. M : keyword (marking); deadlock, bounded: keywords; • Incompatibility: A composite net N is incompati- i, j:place indexes; a, b, k :integers ; ∗, +, −, and, or, ⇒ ble if it is neither partially nor totally compatible. , not: usual operators ; p, q: GMEC We focus in what follows on formulating the four The syntax (p) → [0, b](q) denotes a leads to types of compatibility properties. Let us consider the property meaning AG((p) imply AE[0, b](q)). E.g. following notation: (p) → [0, b](q) holds iff whenever p holds eventually q will hold as well in [0, b] time units. • nbX: the number of processes; 3.2. TCTL characterization of ToWF-nets • nbp: the number of places in a given process; compatibility • nbi: the number of interface places in a In a composition of two or more processes, composition; the correctness of the composite process refers • is : the input place of the process number s. in general to the compatibility of the different processes. From a behavioral point of view, the • fs : the output place of the process number s. involved processes are compatible if they can interact properly. This means that composite process Partial compatibility • Partial compatibility of nbX processes refers to the where nbip is used to denote the number of places absence of deadlock in their composition. A net other than the final place in a process. is deadlock-free if and only if there is at least a transition allowed in every marking except the final Perfect compatibility one Mf in which refer to the marking of all the final places fs (s = 1..nbX). This property is expressed When we have a strict overall deadline that the as follows: system should respect, we can enforce the total compatibility by adding this constraint. We define, in ∀M ∈ [M0 i, Mf in ∈ [M i this sense, the perfect compatibility which refers to both deadlock-freeness and proper termination while Logically, this deadlock-freeness property can be taking into account the deadline verification. expressed as follows: "for all the executions made Let us suppose that the deadline constraint is possible from the initial state, no deadlock is considered, this can be checked by verifying that a encountered until the final state is reached". The process has to terminate (reach its final state) in T m final state is characterized by the marking of the time units. Which lead to the expression of the proper final places. Then, we can express the partial termination within this delay as follows: compatibility by the following TCTL formula: AF[0,T m] StrictM F AG[0,∞[ ((not M F ) ⇒ not deadlock) Hence, these two TCTL formulas can be used In this formula, deadlock is a proposition supposed to to express the perfect compatibility of ToWF-nets return true if and only if there is no enabled transition composition: in the current state. M F is a proposition on marking Mf in assuring that each final place is marked with at • AG[0,T m] ((not M F ) ⇒ not deadlock) least one token. • AF[0,T m] StrictM F nbX M F = ∧ M (fs ) >= 1 s=1 Incompatibility Here we check only the marking of final places. The incompatibility is a situation in which neither deadlock-freeness nor proper termination is verified. Total compatibility In other words, a set of ToWF-nets are incompatible if all the possible executions don’t lead to final The proper termination of a process refers to check if states of the different processes. We may distinguish this latter complete its execution in any case, and at here between strong incompatibility checked in the the time of termination, all the places of the involved interval [0, ∞[ and weak incompatibility which refers ToWF-nets are empty except the final places which to incompatibility in a limited interval [a, b]. must be marked with exactly one token. Hence, we have to check if there exists a marking M for which If we consider that the interval [x, y] may correspond all the places are empty except the output ones. to [0, ∞[ or [a, b], the expression of the incompatibility Formally, this property can be expressed as follows: in TCTL leads to the following formula: ∀M ∈ [M0 i : PnbX AG[x,y] ((not M F )) M (fs ) ≥ 1 ∀s ∈ {1, .., nbX} ⇒ M = s=1 fs 3.3. Model checking ToWF-nets composition We can formulate the proper termination in TCTL as We present in this subsection some results related follows: to the analysis of the compatibility and soundness properties for a ToWF-nets composition. This AF[0,∞[ StrictM F verification is ensured by Romeo (Gardey et al. (2005)) which is a software studio dedicated to time With StrictM F a proposition on the marking with a Petri nets analysis. Romeo is developed by the token in every final place fs but no tokens in the other Real-Time Systems Team at IRCCyN. It performs places including the interface ones. analysis on Transition Time Petri Nets as well as nbip on one of their extensions dedicated to scheduling. nbX StrictM F = ∧ ( ∧ (M (p) = 0) Romeo is chosen because it assures, among other s=1 p=1 nbi features, a State Class Graph (SCG) computation ∧ (M (fs ) = 1)) ∧ ( ∧ M (Ii ) = 0) and a graphical simulation of Transition Time Petri i=1 Nets. Moreover, Romeo is used here because it • implements an on the fly model checking algorithm of TPN-TCTL formulas. We propose to study a simple composition of ToWF- nets (figure 1). We can easily verify that no deadlock will be encountered until final places are marked. Then the partial compatibility is satisfied (see figure 2). However, the firings of transitions T4 and T5 of the second ToWF-net lead to two tokens in its final place f2 ; this violates the total compatibility property. In the figure 3, we show the result for this property and an execution trace. After that, we propose a correction in figure 4 for which the total compatibility is verified (see figure 5). Figure 3: Total compatibility is not verified Figure 1: Example 1 of ToWF-nets composition Figure 4: Example 2 of ToWF-nets composition Figure 2: Partial compatibility is verified Figure 5: Total compatibility is verified 4. PARAMETRIC ANALYSIS OF TOWF-NETS In this section, we tackle with a parametric tokens in the beginning of each process and these quantitative analysis of the composition of ToWF- tokens will be used and released after their use, nets. This suppose to consider k instances of each i.e. at the end of execution, the resource places will ToWF-nets ready to be executed. regain their same initial markings. For sake of covering the maximum number of real For this, we define the time open WF-nets with world processes, we tackle with time processes shared resources (ToWFR-nets) which stand for a which share resource places. This places possess • class of Petri nets dedicated to model workflow processes with: time delays, resource places as well as interface places. Definition 5 (ToWFR-net) A ToWFR-net N is a tuple (P, RP, T, F, RF, F I, I, O, WRP , M0 ) with: • (P, T, F, F I, I, O) is a ToWF-net, • RP is a set of resource places, • I, O, P and RP are disjoint, • RF ⊆ (RP × T ) ∪ (T × RP ) is the flow relation for resources, • WRP : RF 7→ N is the weight function defining the weight of arcs linking the resource places. To ensure the use of resource places, we require: WRP (u) ≥ 1∀u ∈ RF • M0 is the initial marking: M0 = k.i + MRP where k is the number of tokens in the initial place i and MRP is the marking of resource places. For the interaction of ToWFR-nets, we use only interface places; resource places are used to model resources sharing between activities of the same process. In the sequel, we will use these notations: • IOj refers to interface place number j Figure 6: Composition of three machines’ processes • RPj refers to resource place number j. As an example of ToWFR-nets composition, we study a manufacturing lane of three machines which The k-partial compatibility refers to verify if all collaborate together to manufacture some product. the instances of the involved processes terminate The composite net describing the manufacturing without encountering a deadlock. This is possible workflow is given in figure 6. by extending the deadlock-freeness specified in the previous section with a test of the termination of the In this example, each machine will be launched twice k instances. This can be specified by the following (2 tokens in each initial place ij ) and share an TCTL formula: internal resource modeled by RPj with j the number nbX of machines. The three machines communicate via AG[0, ∞[(not( ∧ (M (index_of _fs ) >= s=1 the two interface places IO1 and IO2 . k)) => not deadlock) Now, to verify if the interacting ToWF-nets commu- Where nbX is the number of involved processes nicate correctly and if their collaboration process is sound, we propose to extend the above classes of For the three machines example (6) this formula is compatibility properties with the consideration of the written in Romeo as follows: concurrent instances ready for execution. AG[0, inf ](not(M (4) >= 2 and M (7) >= 4.1. K-compatibility analysis 2 and M (26) >= 2) => not deadlock) We define the following formulas: the k-partial compatibility and the k-total compatibility. Where 4,7 and 26 are the indexes attributed by Romeo to the three final places. k-partial compatibility • The figure 7 shows that the two-partial compatibility is guaranteed for the three machines example. Figure 8: Analysis example of the two-total compatibility Figure 7: Analysis example of the two-partial compatibility ToWF-nets composition. Let us consider N the time workflow net obtained by composing the involved k-total compatibility ToWF-nets and the adding of two special places pstart and pend and two transitions tstart and tend The k-total compatibility refers to verify if all which connect respectively pstart to the the input the instances of the involved processes terminate places of the different ToWF-nets and the different properly. This means that we have to verify if final places to pend . we reach the state in which final places have k tokens and resource places regain exactly their initial We can easily prove that if the involved ToWF-nets marking and all the other places are empty. This can are totally compatible then N is sound. In addition if be specified by the following TCTL formula: the ToWF-nets are k-totally compatible then N is k- sound. But the reverse is incorrect, i.e. N is k-sound nbX 9 the ToWF-nets are k-totally compatible. AF [0, ∞[( ∧ (M (index_of _fs ) = s=1 nbR k) ∧ ∧ (M (index_of _RPj ) = j=1 5. RELATED WORK nbop mRPj ) ∧ ∧ (M (index_of _Pj ) = 0)) Several works dealt with the analysis of compatibility j=1 properties of processes modeled by open workflow Where nbX refers to the number of interacting nets or by other formalisms. Wil M. P. van der Aalst processes, nbR refers to the number of resource and al. (van der Aalst et al. (1998)) showed that two places, mRPj refers to the initial marking of resource or more processes are compatible if their interfaces place RPj and nbop refers to the number of places are compatible and there are no deadlocks. In which are neither final places nor resource places. addition, other concepts were formulated in relation with compatibility such as strategy and controllability. For the three machines example (6) this formula is written in Romeo as follows: Marlon Dumas and al. (Dumas et al. (2008)) studied the incompatibility of Web services and classified AF [0, inf ](M (4) = 1 and M (7) = 1 and M (26) = it into two types such that the incompatibility of 1 and M (27) = 1 and M (16) = 1 and M (3) = signatures and the protocol incompatibility. The 1 and M (1) = and M (2) = 0 and M (5) = former occurs when a service requests an operation 0 and M (6) = 0 and M (8) = 0 and M (9) = which is not possible from another service. The 0 and M (10) = 0 and M (11) = 0 and M (12) = latter occurs when a service enters in a series of 0 and M (13) = 0 and M (14) = 0 and M (15) = interactions with an other service, but there is no 0 and M (17) = 0 and M (18) = 0 and M (19) = compatibility in the two services orders. 0 and M (20) = 0 and M (21) = 0 and M (22) = 0 and M (23) = 0 and M (24) = 0 and M (25) = 0) Lucas Bordeaux and al. (Bordeaux et al. (2005)) tackled the verification of Web services compatibility The figure 8 shows that the two-total compatibility is while assuming that not only the exchanged guaranteed for the three machines example. messages are semantically of the same type but also they have the same name. For the modeling After these tests, we highlight some results on of Web services, their work is based on labeled the characterization of quantitative properties of transition systems (LTS). The authors defined three • types of compatibility: absence of deadlock, opposite on Structure Theory of Petri Nets. International behavior and unspecified reception. Journal of Computing and Information Sciences (IJCIS), pp. 51-61. Wei Tan and al. (Tan et al. (2009)) proposed an approach that checks interface compatibility of Web Berthomieu, B. and Diaz, M. (1991) Modeling and services described by BPEL, and corrects these verification of time dependent systems using services if they are not compatible. To do this, they time Petri nets. IEEE Transactions on Software modeled the composition by SWF-nets, a subclass Engineering, 17(3). of CPN (Colored Petri Nets). Then they checked the Bordeaux, L. and Salaun, G. and Berardi, D. and compatibility of interfaces. Mecella, M. (2005) When are two web services While these approaches dealt with non time compatible ?. Sapienza University, 3324. processes, we focused on those constrained by time Boucheneb, H. and Barkaoui, K. (2013) Reducing information. To check the compatibility of interacting interleaving semantics redundancy in reachability processes, we chose to extend oWF-nets with delays analysis of time Petri nets. ACM Transactions in associated to activities. In addition, we were based Embedded Computing Systems (TECS), 12(1), pp on the formal verification in our approach. We mainly 1-24. used the model checking formal method to check the compatibility classes of ToWF-nets, which shows Boucheneb, H. and Barkaoui, K. (2012) Paramet- a counter example in case a property is violated ric Verification of Time Workflow Nets. 24th In- allowing thus to recognize and correct the eventual ternational Conference on Software Engineering errors as early as possible. (SEKE), pp 375-380. Berthomieu B. and F. Vernadat F. (2003) State class 6. CONCLUSION constructions for branching analysis of time Petri nets. TACAS 2003, volume 2619 of Lecture Notes Nowadays, technological progress plays a funda- in Computer Science, pp 442-457. mental role in the optimization of production pro- cesses in different sectors, especially facing the va- Dumas, M. and Benatallah, B. and Motahari rieties produced and the constraints of productivity, Nezhad, H. (2008) Web Service Protocols : capability, quality and competitiveness. For this, a Compatibility and Adaptation. Institute of Electrical prior verification of such processes and their inter- and Electronics Engineers. action is tremendous. Guermouche, N. and Perrin, O. and Ringeissen, We proposed first in this paper a model for C. (2008) Timed Specification For Web Services processes interaction based on Petri nets. Then, Compatibility Analysis. Theoretical Computer Sci- we studied the compatibility of these processes by ence. model checking techniques. In particular, we applied Hadjidj, R. and Boucheneb, H. (2009) On-the- a TCTL model checking of these properties and Fly TCTL Model-Checking for Time Petri Nets. simulated some examples on the Romeo model Theoretical Computer Science, 410(42), pp 4241- checker. Finally, we enhanced these results by taking 4261. into account several instances ready for execution as well as a possibility of sharing resources. Hence, Camerzan, I. (2007) On Soundness for Time we introduced to parametric verification of interacting Workflow Nets. Computer Science Journal of processes. In future, we propose to strengthen this Moldova, 15(1), pp 74-87. parametric analysis of ToWF-nets and ToWFR-nets. De Michelis, G. and Ellis, C. and Memmi, G. (1994) Proceedings of the second Workshop REFERENCES on Computer-Supported Cooperative Work, Petri nets and related formalisms, Zaragoza, Spain.. Alur, R. and Courchoubetis, C. and Dill, D. (1993) Model checking in dense real time. Information Foster, H. and Uchitel, S. and Magee, J. and Kramer, and computation (104). pp 2-34. J. (2004) Compatibility Verification for Web Service Choreography. Proceedings of IEEE International Atluri, V. and Huang, W. (1996) An authorization Conference on Web Services, pp 738-741. model for workflows. Proceedings of the 4th European Symposium on Research in Computer Ellis, C. and Keddara, K. and Rozenberg, G. Security, London, Springer-Verlag. pp 44-64. (1995) Dynamic change within workflow systems. Proceedings of conference on Organizational Barkaoui, K. and Ben Ayed, R. and Sbaï, Z. computing systems, pp 10-21. (2007) Workflow Soundness Verification based • Esparza, Javier and Silva, Manuel (1989) Circuits, Tan, Wei and Fan, Yushun and Zhou, MengChu handles, bridges and nets. Applications and (2009) A Petri Net-Based Method for Compatibility Theory of Petri Nets, Lecture Notes in Computer Analysis and Composition of Web Services in Science, 483, pp 210-242. Business Process Execution Language. IEEE T. Automation Science and Engineering, 6(1), pp 94- Martens, A. (2003) On Compatibility of Web 106. Services. Petri Net Newsletter, pp 12-20. Yoneda, T. and Ryuba, H. (1998) CTL model Gardey, G. and Lime, D. and Magnin, M. and Roux, checking of time Petri nets using geometric O.H. (2005) Romeo: A Tool for Time Petri Nets regions. IEICE Transactions on Information and Analysis. Proceeding of 17th International Confer- Systems, pp 297-396. ence on Computer Aided Verfication (CAV’05), vol- ume 3576 of Lecture Notes in Computer Science, van der Aalst, W.M.P. and Arjan, J.M. and pp 418-423. Christian, S. and Wolf, K. (1998) Service Interaction: Patterns, Formalization, and Analysis. Gou, H. and Huang, B. and Liu, W. and Li, Y. 9th Internatinal School on Formal Methods for the and Ren, S. (2001) Modeling distributed business design of Computer, Communication and Software processes of virtual enterprises based on the Systems. object-oriented approach and petri nets. Systems Man and Cybernetics. van der Aalst, W.M.P. (1997) Verification of Workflow Konur, S. and Fisher, M. and Schewe, S. (2013) nets. ICATPN 97, LNCS, 1248. Combined model checking for temporal, proba- van der Aalst, W.M.P. (1996) Three good reasons bilistic, and real-time logics. Theoretical Computer for using a petri-net-based workflow management Science, 503, pp 61-88. system. International Working Conference on Ling, S. and Schmidt, H. (2000) Time Petri Information and Process Integration in Enterprises Nets for Workflow Modelling and Analysis. IEEE (IPIC96), pp 179-201. International Conference on Systems, Man, and van der Aalst, W.M.P. (1993) Interval timed coloured Cybernetics, pp 3039-3044. petri nets and their analysis. Proceedings of the Martens, A. (2005) Analyzing Web service based 14th International Conference on Application and business processes. Proceeding of International Theory of Petri Nets, London, Springer-Verlag, pp Conference on Fundamental Approaches to 453-472. Software Engineering, Part of the European Joint Karsten and Schmidt (2005) Controllability of open Conferences on Theory and Practice of Software, workflow nets. EMISA. LNI, Bonner Köllen Verlag, Lecture Notes in Computer Science vol. 3442. pp 236-249. Massuthe P. and Reisig W. and Schmidt K. (2005) An Sbaï. Z. and Kamel Barkaoui. and Hanifa Bouch- Operating Guideline Approach to the SOA. Annals eneb. (2014) Compatibility Analysis of Time Open of Mathematics, Computing and Teleinformatics, Workflow Nets. Proceedings of the International pp 35-43. Workshop on Petri Nets and Software Engineer- Ridi, L. and Torrini, J. and Vicario, E. (2012) ing, co-located with 35th International Conference Developing a Scheduler with Difference-Bound on Application and Theory of Petri Nets and Con- Matrices and the Floyd-Warshall Algorithm. IEEE currency (PetriNets 2014) and 14th International SOFTWARE. Conference on Application of Concurrency to Sys- tem Design (ACSD), pp 249-268. Sbaï, Z. and Barkaoui, K. (2013) Vérification formelle des processus workflow - Extension aux work- Sbaï. Z. and Kamel Barkaoui. (2014) On Compat- flows inter-organisationnels. Revue Ingénierie des ibility Analysis of Inter Organizational Business Systèmes d’Information: Ingénierie des systèmes Processes. Enterprise and Organizational Model- collaboratifs, 18(5), pp 33-57. ing and Simulation - 10th International Workshop, EOMAS 2014, Held at CAiSE 2014, Thessaloniki, Sbaï, Z. and Barkaoui, K. (2012) Vérification Greece, June 16-17, 2014, Selected Papers, pp Formelle des Processus Workflow Collaboratifs. 171-186. Actes de la conférence francophone sur les Systèmes Collaboratifs (SysCo’12), pp. 197-210. Boucheneb, H. and Gardey, G. and Roux, O.H. (2009) TCTL model-checking of Time Petri Nets. Journal of Logic and Computation, 19(6), pp 1509- 1540.