Business process modeling is still a challenging task especially since more and more aspects are added to the models, such as data lifecycles, security constraints, or compliance rules. At the same time, formal methods allow for the detection of errors in the early modeling phase. Detected errors are usually explained with a path from the initial to the error state. These paths can grow unmanageably and make the understanding and fixing of errors very time consuming. This paper addresses this issue and proposes a more intelligible explanation of errors: Instead of listing the actions on the path to the error, only which decisions lead to it are reported and highlighted in the original model.
Niels Lohmann
Business process modeling is a sophisticated task and received a lot of attention in the past decades. With the advent of domain-specific languages and a growing scientific community, the act of creating and managing business process models has become a discipline on its own. Despite all eforts, design flaws may still occur. This can have diferent impacts, ranging from syntactically incorrect models, which are harder to understand, up to catastrophic faults and down times in the execution that yield to a loss of money or a legal aftermath. Consequently, a large branch of research focuses in the detection, correction, and avoidance of errors in business process models. Whereas plain control flow analysis is now well understood, other aspects such as data, business rules, or security may introduce more subtle flaws that are harder to detect.
Using the prominent soundness [
Due to the ongoing evolution of business process modeling languages, the growing number of aspects that need to be covered by a business process model, or the trend toward executable business process models, the vericfiation of business process models has become a moving target. As a consequence, specific approaches may become inapplicable for novel demands, leaving only general purpose approaches as stable tools for the future.
Problem description. In principle, a model checker takes a formal model (e.g., a
Petri net) and a formal description of the property to check (usually described
by temporal logic formula φ ) as input and tries to prove the property by an
exhaustive investigation of the model’s states. In case the property is violated
(e.g., a deadlocking state is detected), a path π to this error state is reported [
Unfortunately, the size of the paths correlates with the size of the model and paths of industrial models can thus be very long and hardly understandable. Furthermore, the path can contain a lot of irrelevant or diverting information that makes the comprehension of the error very dificult. For instance, the path usually contains actions that only “set up” the process (e.g., initializations and login procedures). These inevitable actions are certainly necessary to be able to reach the error state, but are usually not the cause of it. Another aspect that makes paths hard to understand is the fact that business process models may span several components where activities are executed in parallel. On the path, these originally unordered activities are reported in a fixed — and possibly arbitrary — order which may yield confusion due to unintuitive error descriptions. Contribution. This paper addresses the mentioned problems by shortening paths by focussing on the choices made rather than on each individual action. We shall use a large case study as experimental evaluation of our proposed approach. 2
Business process modeling languages are usually semiformal and hence are not
directly applicable to a mathematically rigorous proof of correctness criteria.
However, the operational semantics can be captured in formalisms such as Petri
nets or process calculi. With the advent of executable languages such as WS-BPEL
2.0 or BPMN 2.0, such a formalization became much easier, because a precise
execution semantics yielded more careful language specifications. In fact, for most
of today’s languages from industry or academia, translations into Petri nets [
Example. Figure 1(a) depicts a small business process model from [
M1
M2
J1
(a) business process model from [
F1 t4 p5
t5
p1
t1
t8
p2
t2
p3
t3
t9
p4
Model checking [
For the remainder of the paper, we use model checking tool LoLA [
Example (cont.). The business process from Fig. 1(a) has a lack of synchronization. This can be detected by checking the Petri net from Fig. 1(b). The following path π describes how a marking m can be reached which puts two tokens on place p6. π = t1 t2 t9 t10 t11 t12 t14 t8 t2 t3 t4 t5 The path contains 12 transitions. In the remainder of this paper, we use this path to exemplify the proposed reductions.
It is worthwhile to mention that model checking sufers a devastating worst
case complexity due to the well-known state explosion problem which yields
reachability graphs with exponential blow-ups compared to the size of the models.
However, even industrial business process models can be model checked in few
microseconds, because heuristics that fight the state space explosion proved to
be very efective in this domain [
3.1
The problem: long paths = big problems In the remainder of the paper, we focus on the following problem: Given a path π to a goal marking m of a Petri net model N , how can the reason for the error modeled by m be briefly and comprehensively explained to the modeler of N ?
Apparently, π describes how the goal marking m can be reached from the initial marking m0 of N . Consequently, reporting the transitions of π together with the intermediated markings to the modeler should help to understand the reasons m was reached. Unfortunately, this approach is futile in case π contains dozens of transitions. The reasons for such long paths are: Detours: Model checkers usually investigate the markings of a Petri net in a depth first search 1. As a result, the reported paths do not need to be optimal and may contain some transitions that model “detours” in the reachability graph that do not contribute in the actual reaching of the goal marking. Interleaving of concurrent transitions: A marking of N may activate two transitions t1 and t2 which are not mutually exclusive. That is, firing either transition first does not disable the other one. A typical reason for this is that t1 and t2 do not share any resources. Consequently, the order in which t1 and t2 occur on the path π is arbitrary. If each transition belongs to diferent components of the underlying business process model, then these arbitrary interleaving of the transitions may be irritating to the modeler if she tries to understand the path π. In the example path, transition t11 and t12 are concurrent and the reported order in path π (t11 before t12) is arbitrary. Indisputable parts: Though the path π is an actual proof that the goal marking m can be reached in N , not every transition on the path is an actual cause of m. In the example process, any path will begin with firing t1 and hence does not need to be reported to the modeler as reason for an error. 1 Breadth-first approaches are not applicable to many classes of formulae.
The solution: don’t report the obvious To tackle the problem of long paths with redundant or unhelpful information, we shall exploit two aspects to shorten paths in the remainder of this section: progress and conflicts .
Progress is the assumption that the model never “gets stuck” in case a transition is activated. That is, if a marking activates one or more transitions, then this marking is eventually left by firing on of these transitions. Progress is a natural assumption for business process models in which the execution of tasks also cannot be postponed indefinitely. Though the actual occurrence of message or timer events cannot be precisely predicted, the respective states are always assumed to be eventually left by the modeled actions.
A conflict is a situation in which there exist more than one possible
continuations (e.g., an XOR gateway). In terms of Petri nets, it is a marking in which
two transitions t1 and t2 are enabled, but after firing either of them, the other
transition is disabled. This situation is dual to concurrent transitions (see above)
that do not disable each other. A detailed discussion of these aspects can be
found in [
The combination of these aspects brings us to the following intuitive observation: Only the conflicts on the path π carry information on how to reach the goal markings. Any other marking m on the path between the initial and the goal marking either (1) enables no transition: Then this must be the goal marking itself, because it has no successor marking. Alternatively, (2) marking m enables exactly one transition: Then this transition is eventually fired due to the assumption of progress. Consequently, this transition does not need to be reported to the modeler as its rfiing was already determined by the previous transition on π thad lead to m. Finally, (3) marking m enables several concurrent transitions. These transitions may fire independently, and if all of them are on π, then the exact order is arbitrary.
Example (cont.). The conflicts of our running example are shaded gray in
Fig. 1(b): transitions t3 and t9, as well as t13 and t14 are conflicting. As a result,
we can reduce the path π as follows:
πreduced = t9 t14 t3
The firing of all other transitions is clear from the context from the intermediate
markings and the assumption of progress. Note that the transition names need to
be translated back into the terms of the original model. A diferent representation
of πreduced could be: “After (1) decision D1: No, (2) decision D2: No, and (3)
decision D1: Yes, a lack of synchronization occurs after after merge M2.” This is
depicted in Fig. 2.
To evaluate the path reduction algorithm, we applied it to a large collection of
industrial process models created by IBM customers using the IBM WebSphere
translation, we therefore assumed that each input set can potentially activate each output
set. Two di↵ erent translations into workflow graphs and Petri nets were implemented,
although the Petri nets could also be directly obtained from the workflow graphs by a
well-known construction [
Intuitively, a transition ti on a reduced path π is a spurious conflict if every transition t in conflict to ti eventually reaches the marking mi+1 which enables the next transition ti+1 on path π. In this case, choosing any transition from the ith conflict will eventually enable the next conflict on the path to the goal state. Consequently, reporting the spurious conflict ti is of little help to the modeler to understand the error itself.
The check for spurious transitions denfied above can be straightforwardly be implemented using a model checker.3 We integrated this check as postprocessing 2 The original models and their Petri net translations are available for download at http://service-technology.org/soundness. 3 We check whether N with initial marking m′i satisfies the CTL formula φ = AF mi+1. step after reducing the paths as described in the previous section. Note that executing a model checker can be very time and memory consuming. However, even if a check is not finished with a reasonable amount of resources, we just failed to proof whether a conflict is spurious and can continue with the investigation of the next transition. That said, the postpocessing can be aborted at any time — any intermediate result is still correct.
We applied the reduction of spurious conflicts to the case studies described in the previous section. Table 4–6 summarize the results. In all three experiments, the paths could be further reduced by 50–86%. Note that in some cases, the check for spurious conflicts has been aborted after more than 2 GB of memory were consumed. In these cases, the conflict was kept in the path and the check proceeded with the next conflict. 5
Related work. The analysis and verification of business process models is a
broad field of research. Consequently, there exists a variety of domain-specific
approaches (e.g., the decomposition of workflow graphs into SESE regions to check
soundness [
Related to the presentation of error information is the automated correction
of flawed business process models [
A to find a correct business process model which maximally resembles the flawed model. These approaches have the benefit of avoiding lengthy manual correction steps altogether.
Future work. In this paper, we focused on reducing paths to error states and
neglected the retranslation into the original business process model. Visualizations
such as Fig. 2, possibly enriched with animations, need to be automated and
evaluated by business process modelers. Here, understandability criteria [
We see in this paper a first step toward a diagnosis framework which uses general purpose verification tools to verify business process models. As motivated in the introduction, domain-specific approaches are very closely coupled to the structure or the property under investigation, but may become inapplicable for future developments. In contrast, the modularization (a translation into Petri nets as frontend, a general purpose model checking tool as middleware, and a diagnosis framework as backend) may be more flexible when it comes to novel business process languages and properties.