A Data-Centric Approach to Deadlock Elimination in Business Processes Christoph Wagner Institut für Informatik, Humboldt Universität zu Berlin, Unter den Linden 6, 10099 Berlin, Germany cwagner@informatik.hu-berlin.de Abstract. In this paper, we sketch a data-centric approach to avoid deadlocks of a business process. If dependencies between data values are neglected or modelled incorrectly, this can lead to errors in the control flow of the business process. We address the problem of detecting deadlocks which are caused by the improper handling of data. We show by example, how these deadlocks can be detected by means of a symbolic reachability graph. Under certain conditions, we can derive the correct dependency between the involved data values. This allows to modify the business process in a way so that the detected deadlocks will not be reachable. 1 Background The design of business processes is an error prone task. This motivates the use of formal verification to help a business process designer to avoid certain kinds of errors. Models of business processes can be transformed into more formal models like process algebra [4] or Petri nets [9,7]. A business process can also be designed as a Petri net directly (e. g. with CPN Tools [10]). These models can be checked for soundness and other properties by means of formal verification. However, little attention has been paid to the influence of data on the correct- ness of a business process. Most formal models represent data only in a highly abstracted and imprecise form. Models that explicitly include data usually have a clear separation between the control flow part and the data part [3]. Often, the dependencies between data flow and control flow are not very complex, i. e. there is only a small set of values a data item can have. For many the properties in focus of recent research, the actual value of a data item is not important [12], [13] and primarily concerns the order in which read and write activities on variables are carried out. E. g., reading an uninitialized value is considered an error. In this paper, we consider processes that are heavily influenced by data and might be unable to finish a task for some combinations of data values. Technically, this means that a deadlock is reachable under some conditions. Our goal is to find out those harmful combinations of data values and describe the relation the value must adhere to in order to avoid a deadlock (e. g. in the form of a function) and use this information to fix the process. Concerning this aspect, our approach is more general than the approach of [1] which does not deal with relations between data values. We represent a business process by a High-Level Petri net [5]. A High-Level Petri net is an extension of a Petri net where places are typed, tokens have values of the respective type and arcs are inscribed with terms. When a transition fires, values are assigned to the variables appearing in the inscriptions of adjacent arcs. The evaluation of the inscriptions determines which values are produced and consumed. The terms are evaluated with a fixed interpretation (note that the Petri net is not a schema in the sense of [11]). We do not exploit restrictions on the Petri net’s structure that a certain business process modelling language might impose. This allows us to handle more general models (e. g. as obtained from CPN Tools). We assume that the Petri net is bounded, acyclic and fulfils some technical requirements of minor importance which do not restrict the expressivity and will not be mentioned here. The restriction to acyclic nets can be relaxed as long as computational issues are neglected. We assume that the set of values used by the Petri net can be so large that an explicit enumeration would be computationally inefficient. start start x id(x) y x id(x) y order id order id manu- manu- facture facture receive [x=y] receive [x=y] exp. exp. prod. x y id-1(y) prod. x y z product product stop stop customer manufacturer customer manufacturer (a) Correct business process (b) Incorrect business process Fig. 1: Business process consisting of a customer an a manufacturer, represented as a Petri net Consider a business process formed by a customer and a manufacturer (Fig. 1a). The customer orders a product x from the manufacturer by telling the man- ufacturer the product’s id (order). The manufacturer assembles the product associated with the id and returns the product to the customer (manufacture). Let us now assume that due to a design error in the manufacturer’s internal workflow, the id y obtained from the customer is lost and replaced by the id of an arbitrary product z (Fig. 1b). Then, the customer will get a product different from the one he expects. In that case, no further action (receive) can be performed because the condition x = y is not satisfied and we reach a deadlock. We call this a conditional deadlock, because it occurs only if the compared data values are not equal. Note that in a more complex scenario, a choice dependent on data may not always lead to a deadlock instantly but later on in the process. In that case, the deadlock condition has to be propagated backwards. This aspect will not be covered in this paper. We introduce an approach to detect conditional deadlocks and to derive the dependency between values that must be used in order to avoid the deadlock. In Sect. 2, we illustrate by simple examples, how to identify deadlocks by means of a symbolic reachability graph. Section 3 shows by a more sophisticated example, how to derive the precise conditions under which an conditional deadlock can be avoided. It is not always possible to derive these conditions precisely. Section 4 shows an example that can not be corrected with our approach due to imprecise results. In Sect.5, we conclude our work. 2 Basic Idea In this section, we show how to detect a deadlock by means of the symbolic reachability graph (SRG) of the Petri net. In the following examples, we assume that every place has the type integer except for some places that carry tokens (denoted as black dots) that do not have a value. A marking m of a Petri net N is considered a deadlock, if no transition is enabled and m is not contained in a set Ω of final markings of N . In each of the following exam- p0 p0 ples, we assume that the net is in t0 t0 [x 0] a final marking exactly when the x x place pΩ is marked. Consider the p1 [ p0 ] p1 net N1 in Fig. 2a. We can easily see x t0 x that N1 is not deadlock free and t1 [x 0] [ p1=V0 ] t1 [x 0] M = {[p1 = n]|n ∈ Z, n < 0} is x t1 x the set of deadlocks reachable in pΩ [ pΩ=V0, V0 0 ] pΩ N1 . Obviously, by adding the guard (a) N1 (b) SRG(N1 ) (c) N10 x ≥ 0 to t0 , we can ensure that t1 will always be enabled and N1 will Fig. 2: Net with a conditional deadlock and eventually reach the final marking its correction [pΩ ] (Fig. 2c). In a marking of the symbolic reachability graph, every value is represented by a term. Without going into technical details, we show how to construct the symbolic reachability graph of N1 . Starting from initial marking [p0 ], t1 produces an arbitrary integer on p1 (Fig. 2b). We represent this integer by a unique identifier V0 . Thus we get the marking [p1 = V0 ]. While formally V0 is a constant, we treat V0 as a variable: V0 may later be instantiated by any value from Z. Since t1 is enabled only if V0 is non-negative, we keep the condition in V0 ≥ 0 in the successor marking [p2 = V0 , V0 ≥ 0] of [p1 = V0 ] (we obtain the condition by combining the firing mode of t1 and the guard of t1 ). We consider an instance of a marking of the symbolic reachability graph valid, if every condition denoted in the marking evaluates to true. Obviously, a marking of N1 is reachable exactly if it is a valid instance of a marking of the symbolic reachability graph. With the symbolic reachability graph, we can identify under which condition a marking instantiates to a deadlock. Here, [p1 = V0 ] is a conditional deadlock for ¬V0 ≥ 0 since each instance of [p1 = V0 ] has no successor for this condition. We now enforce that the condition V0 ≥ 0 holds in [p1 = V0 ] by adding the guard x ≥ 0 to the predecessor-transition t0 of [p1 = V0 ]. We obtain a corrected version N10 of N1 , which is deadlock free. p0 t0 t2 x x p1 [ p0 ] x x t0 t2 [x<0] t1 t3 [x>0] [ p1=V0 ] [ p1=V1 ] x x t1 t3 t1 t3 pΩ [ pΩ=V0, V0<0 ] [ pΩ=V0, V0>0 ] [ pΩ=V1, V1<0 ] [ pΩ=V1, V1>0 ] (a) N2 (b) SRG(N2 ) Fig. 3: Net with a branching symbolic reachability graph Fig. 3a shows a net N2 which is not deadlock free and which has a branching symbolic reachability graph. Note that the values produced by t0 and t2 obtain different identifiers (although both branches behave symmetrically). [p1 = V0 ] and [p1 = V1 ] are conditional deadlocks of N2 . [p1 = V0 ] is a deadlock for ¬((V0 < 0) ∨ (V0 > 0)). Any successor of an instance of [p1 = V0 ] belongs either to the branch with condition V0 < 0 or the branch with condition V0 > 0. We enforce the condition (V0 < 0) ∨ (V0 > 0) by adding the guard (x < 0) ∨ (x > 0) 6 0). By repeating this procedure for to t0 (which is effectively equivalent to x = [p1 = V1 ], we get the same guard for t2 and obtain a deadlock free net. 3 Derivation of a deadlock-preventing guard In the previous section, we have shown that by adding an appropriate guard, we can prevent the reachability of deadlocks. Adding a guard or replacing a guard by a more restrictive one makes the net less permissive, that is the set of reachable markings gets smaller. Naturally, we want to prevent all deadlocks from being reachable. On the other hand, we do not want to prevent the reachability of more markings than necessary. This section addresses the issue of deriving a least restrictive guard. How to derive a guard (like x > 0) from a condition (like V0 > 0) is not obvious if more than one variable is involved and functions are used in the arc inscriptions. Without loss of generality, we assume that the symbolic reachability graph is a tree (if not, we can unfold it). Note that the symbolic reachability graph usually has an acyclic structure since names of value identifiers never repeat. In the tree, we always modify the guard of the transition that directly precedes the deadlock. It should be mentioned here, that due to restrictions inherent to the modelled the business process (e. g. the dependency on of external events which can not be influenced), it might not be possible to modify that transition. In that case, we choose the first modifiable predecessor transition in the tree. As guard derivation is more involved in that case, it will not be shown here. Consider the net N3 in Fig. 4a, which reaches a deadlock if the integer produced by t1 on p3 is greater than the integer produced by t0 on p1 . An ad-hoc way to fix N3 is to add the guard z ≥ y to t1 . Then, N3 eventually reaches the final marking [pΩ ]. However, the guard z ≥ y − 1 would also ensure that N3 reaches [pΩ ] but is less restrictive than x ≥ y, since it evaluates to true for more assignments of x and y. The guard y = 6 ∨ z ≥ y − 1 is even less restrictive than z ≥ y − 1. We derive this guard from the symbolic reachability graph in Fig. 4b. m0 is a deadlock for condition ¬(V0 ≤ V1 ) since ev- p0 00 ery valid instance of m satis- t0 [x≠5] fies V0 ≤ V1 . We prevent the 0 x x+1 reachability of m under condi- p p2 1 tion ¬(V0 ≤ V1 ) by adding a y guard to t1 . It is sufficient that t1 [ p0 ] the guard forbids the violation of x z t0 V0 ≤ V1 only for valid instances p3 [ p1=V0, p2=V0+1, V0≠5 ] (=m) of m and m0 . So we can assume z t1 a t2 [x z] [ p1=V0, p3=V1, V0≠5 ] that for a step m → m0 (where (=m’) t2 a = t1 hy = V0 + 1, z = V1 i) with pΩ [ pΩ, V0≠5, V0 V1 ] (=m’’) integers V0 and V1 given (1) the condition V0 6= 5 already (a) N3 (b) SRG(N3 ) holds (precondition in m) Fig. 4: A net that is less obvious to correct (2) y and z are bound to the val- uations of V0 + 1 and V1 (firing mode of t1 ). This motivates the definition of the expression ∀V0 , V1 ∈ Z : V0 6= 5 ∧ y = V0 + 1 ∧ z = V1 =⇒ V0 ≤ V1 a We call this expression least restrictive V0 ≤ V1 -enforcing (for step m → m0 ). Note that the more preconditions an expression has, the less restrictive it is. V0 and V1 are all-quantified because the condition V0 ≤ V1 shall be enforced for any valid instance of m0 . It is easy to see that this expression is indeed equivalent to y = 6 ∨ z ≥ y − 1. Since V0 , V1 are uniquely determined by y and z, we can replace V0 by y − 1 and V1 by z, thus eliminating V0 , V1 from the expression. We go back to the business process introduced in Fig. 1a. The reader may believe that there is a deadlock m0 = [exp. prod. = V0 , product = V1 ] for condition ¬(V0 = V1 ) which is reachable from m = [exp. prod. = V0 , id(V0 )] via transition manufacture. This leads to the expression ∀V0 , V1 ∈ Z : y = id(V0 ) ∧ z = V1 =⇒ V0 = V1 , which is equivalent to z = id−1 (y). Thus we have reconstructed the dependency between products and their id’s and may correct the business process by replacing z by id−1 (y). In general, several successive deadlock elimination steps are necessary in order to obtain a deadlock free net, as every step may introduce new deadlocks. Our approach is similar to Dijkstra’s method to derive the weakest precondition for which a given program terminates in a specified state [2]. However, our approach allows to derive a modification even for an intermediate step because a precondition and a postcondition are already given. Therefore, we may perform modifications in a local manner and do not have to start at the final markings. Conceptually, the approach is applicable even if no final marking is specified at all. Note that modifying a transition may have non-local side-effects if the transi- tion appears more than once in the tree. In that case, more markings are rendered unreachable than intended, leading to a suboptimal solution. As the next section shows that even without non-local side-effects, it is not always possible to get an optimal solution. 4 Uncorrectable net Some nets can not be corrected using the expression derived in the last section. Consider the net N4 in Fig. 5a. There is no unique way to avoid the deadlocks of p0 p0 p0 [x<5] x x x t0 px t0 px t0 px x p1 p1 p1 x [y 5] y y y t1 py [ p0 ] t1 py t1 py t0 p2 [ p1, px=V0 ] p2 p2 [x [x pΩ [ pΩ, V0