The use of formal semantics for the support of Business Process Management is an emerging branch of research, with substantial economic potential. In particular, business processes modelled in graphical notations such as BPMN can be semantically annotated to specify more precisely what the individual tasks in the process will be responsible for. This raises the need for, and opens up the opportunity to apply, semantic validation techniques: techniques that take the annotations and the underlying ontology into account in order to determine whether the tasks are consistent with respect to each other, and with respect to the underlying workflow structure. To this end, we introduce a formalism for semantic business processes, which combines definitions from the workflow community with definitions from AI; we introduce some validation tasks that are of interest in this context. We then make first technical contributions towards solving this kind of problem. We identify a class of processes where the validation tasks can be solved in polynomial time, by propagating certain pieces of information through the process graphs. We show that this class of processes is maximal in the sense that, with more general semantic annotations, the validation tasks become computationally hard. We outline how the validation information gathered can serve to automatically suggest bug fixes.
One of the promises of service-oriented architectures is increased flexibility through
loose coupling of components. In enterprise applications, Web services can be used to
encapsulate business functionality. The process flow can then, to a large degree, be
separated from the implementation of the process activities. This increased flexibility can
be a key advantage when acting in rapidly changing markets. In such an environment, a
business expert models a business process on a high level of abstraction, like the
Business Process Modelling Notation (BPMN) [
Since modelling is an error-prone activity, the above scenario calls for validation techniques: prior to trying to bind the process, validation should help to ensure that the process model as such makes sense. A validation method may be useful after binding the process, as well: being implemented at a more detailed level, the bound process may reveal flaws that were not visible at the BPMN level of abstraction. Possible validation questions are, for example: Is there an effect conflict, i.e., two tasks with conflicting semantic effects and no ordering constraint between them (simple example: two writeoperations in a database)? Is a particular task reachable, i.e., is there any execution of the process that involves the task? Is a particular task executable, i.e., is its semantic precondition guaranteed to be true when trying to execute it? Answers to these questions are certainly useful as a help for the modeller, and for binding the process; we will see that one can even design techniques that automatically suggest (potential) bug fixes.
Traditional validation techniques, as considered in the workflow community (e.g.
[
Our SBPV formalism is a natural combination of definitions from the workflow
community (e.g. [
We introduce a formalism, i.e., a formal execution semantics, for business processes whose tasks are annotated with logical preconditions and effects (Section 2.1). We then present a number of validation tasks that are of interest for such processes (Section 2.2). We illustrate the formalism with an example annotated BPMN process (Section 2.3). 2.1
Annotated Process Graphs
Our business processes consist of different kinds of nodes (task nodes, split nodes, . . . )
connected with edges. We will henceforth refer to this kind of graphs as process graphs.
For the sake of readability, we first introduce non-annotated process graphs. This part
of our definition is, without any modification, adopted from the workflow literature,
following closely the terminology and notation used in [
Definition 1. A process graph is a directed graph G = (N ; E ), where N is the disjoint union of fn0; n+g (start node, stop node), NT (task nodes), NP S (parallel splits), NP J (parallel joins), NXS (xor splits), and NXJ (xor joins). For n 2 N , IN (n)/OU T (n) denotes the set of incoming/outgoing edges of n. We require that: for each split node n, jIN (n)j = 1 and jOU T (n)j > 1; for each join node n, jIN (n)j > 1 and jOU T (n)j = 1; for each n 2 NT ; jIN (n)j = 1 and jOU T (n)j = 1; for n0, jIN (n)j = 0 and jOU T (n)j = 1 and vice versa for n+; each node n 2 N is on a path from the start to the stop node. If jIN (n)j = 1 we identify IN (n) with its single element, and similarly for OU T (n); we denote OU T (n0) = e0 and IN (n+) = e+.
The intuitive meaning of these structures should be clear: an execution of the process starts at n0 and ends at n+; a task node is an atomic action executed by the process; parallel splits open parallel parts of the process; xor splits open alternative parts of the process; joins re-unite parallel/alternative branches. The stated requirements are just basic sanity checks any violation of which is an obviously flawed process model.
Formally, the semantics of process graphs is, similarly to Petri Nets, defined as a
token game. A state of the process is represented by tokens on the graph edges. Like
the notation, the following definition closely follows [
Definition 2. Let G = (N ; E ) be a process graph. A state t of G is a function t : E 7! N; we call t a token mapping. The start state t0 is t0(e) = 1 if e = e0, t0(e) = 0 otherwise. Let t and t0 be states. We say that there is a transition from t to t0 via n, written t !n t0, iff one of the following holds: 1. n 2 NT [ NP S [ NP J and t0(e) = t(e)
e 2 OU T (n), t0(e) = t(e) otherwise. 2. n 2 NXS and there exists e0 2 OU T (n) such that t0(e) = t(e) t0(e) = t(e) + 1 if e = e0, t0(e) = t(e) otherwise. 1 if e 2 IN (n), t0(e) = t(e) + 1 if 1 if e = IN (n), 3. n 2 NXJ and there exists e0 2 IN (n) such that t0(e) = t(e) t0(e) = t(e) + 1 if e = OU T (n), t0(e) = t(e) otherwise. 1 if e = e0, An execution path is a transition sequence starting in t0. A state t is reachable if there exists an execution path ending in t.
Definition 2 is straightforward: t(e), at any point in time, gives the number of tokens
currently at e. Task nodes and parallel splits/joins just take the tokens from their IN
edges, and move them to their OUT edges; xor splits select one of their OUT edges; xor
joins select one of their IN edges. For the remainder of this paper, we will assume that
the process graph is sound: from every reachable state t, a state t0 can be reached so that
t0(e+) > 0; for every reachable state t, t(e+) 1. This means that the process does
not contain deadlocks, and that each completion of a run is a proper termination, with
no tokens remaining inside the process. These properties can be ensured using standard
workflow validation techniques, e.g. [
For the semantic annotations, we use standard notions from logics, involving logical predicates and constants (the latter correspond to the entities of interest at process execution time).1 We denote predicates with G; H; I and constants with c; d; e. Facts are predicates grounded with constants, Literals are possibly negated facts. If l is a literal, then :l denotes l’s opposite (:p if l = p and p if l = :p); if L is a set of literals then :L denotes f:l j l 2 Lg. We identify sets L of literals with their conjunction Vl2L l. Given a set P of predicates and a set C of constants, P[C] denotes the set of all literals based on P and C; if arbitrary constants are allowed, we write P[].
A theory T is a closed (no free variables) first-order formula. Given a set C of constants, T [C] denotes T with quantifiers interpreted over C. For the purpose of our formal semantics, T can be arbitrary. For computational purposes, we will consider the following standard restrictions. A clause is a universally quantified disjunction of atoms, e.g., 8x::G(x) _ :H(x). A clause is Horn if it contains at most one positive literal. A clause is binary if it contains at most two literals. A theory is Horn (binary) if it is a conjunction of Horn (binary) clauses. Note that binary clauses can be used to specify many common ontology properties such as subsumption relations 8x:G(x) ) H(x) ( ) abbreviates : _ ), attribute image type restrictions 8x; y:G(x; y) ) H(y), and role symmetry 8x; y:G(x; y) ) G(y; x). An example of a property that is Horn (but not binary) is role transitivity, 8x; y; z:G(x; y) ^ G(y; z) ) G(x; z).
An ontology O is a pair (P; T ) where P is a set of predicates (O’s formal terminology) and T is a theory over P (constraining the behaviour of the application domain encoded by O). Annotated process graphs are defined as follows.
Definition 3. An annotated process graph is a tuple G = (N ; E ; O; A). (N ; E ) is a
process graph, O = (P; T ) is an ontology, and A, the annotation, is a partial function
mapping n 2 NT [ fn0; n+g to (pre(n); eff(n)) where pre(n); eff(n) P[], and
mapping e 2 OU T (n) for n 2 NXS to (con(e); pos(e)), where con(e) P[] and
pos(e) 2 f1; : : : ; jOU T (n)jg. We require that: there does not exist an n so that T ^
eff(n) is unsatisfiable or T ^ pre(n) is unsatisfiable; there does not exist an e so that
1 Hence our constants correspond to BPEL “data variables” [
We refer to cycles in (N ; E ) as loops; we refer to edges e for which A(e) is defined
as case distinctions (sometimes, process graphs without loops and/or case distinctions
will be of interest). We refer to pre(n) as n’s precondition, eff(n) as n’s effect
(sometimes called postcondition in the literature), con(e) as e’s condition, and pos(e) as e’s
position. The annotation of tasks – atomic actions that will on the IT level correspond to
Web service executions – in terms of logical preconditions and effects closely follows
Semantic Web service approaches such as OWL-S (e.g. [
Similarly to Definition 1, the requirements stated in Definition 3 are just basic
sanity checks. If a precondition/effect/condition contradicts the theory, then the respective
task node/edge will never be applicable. The requirement on edge positions is a minor
technical detail, stating that no two edges are assigned the same position. This closely
corresponds to standard process languages such as BPEL [
An execution path is a transition sequence starting in a start state s0. A state s is reachable if there exists an execution path ending in s.
Given an annotated process graph (N ; E ; O; A), we will use the term execution path of (N ; E ) to refer to an execution over tokens that acts as if A was completely undefined (in which case Definition 4 essentially simplifies to Definition 2). 2 It is easy to extend our formalism to allow arbitrary formulas for pre(n), eff(n), con(e); extending the actual validation leads to harder decision problems, and remains future work.
The part of Definition 4 dealing with n 2 NP S [ NP J [ NXJ parallels
Definition 2, and should be easy to understand: the tokens pass as usual, and the interpretation
remains unchanged. For n 2 NXS , the definition says that an output edge e0 is
selected where either e0 is not annotated, or e0 has the smallest position among those
edges whose condition is satisfied by the current interpretation, is. Note that this is a
hybrid between a deterministic and a non-deterministic semantics, depending on how
many output edges are annotated. If all edges are annotated, then we have a case
distinction as handled in, e.g., BPEL, where the first case (smallest position) with satisfied
condition is executed (Section 11.2 in [
Let us finally consider the “semantic” part of Definition 4, dealing with task nodes
and their semantic annotations. First, note that we interpret the quantifiers in T over
the constants C that are used in the annotation. The rationale is that the process should
execute based on those entities that are actually available (it remains open to examine
whether it makes sense to drop this assumption). Consider now the start states, of which
there may be many, namely all those that comply with T , as well as eff(n0) if that is
annotated. This models the fact that, at design time, we don’t know the precise
situation in which the process will be executed. All we know is that, certainly, this situation
will comply with the domain behaviour given in the ontology, and with the properties
guaranteed as per the annotation of the start node (if any). The semantics of task node
executions is a little more intricate. If A(n) is undefined, then the logical state i remains
of course unchanged. If A(n) is defined, then pre(n) is required to hold. The tricky bit
lies in the definition of the possible outcome states i0 in the latter case. Our semantics
defines this to be the set of all i0 that comply with T and eff(n), and that differ minimally
from i. This is where we draw on the AI actions and change literature, for a solution to
the frame and ramification problems. The latter problem refers to the need to make
additional inferences from eff(n), as implied by T ; this is reflected in the requirement that
i0 complies with both. The frame problem refers to the need to not change the previous
state arbitrarily – e.g. if a web service makes a booking via account A, then the balance
of account B should remain unaffected; this is reflected in the requirement that i0 differs
minimally from i. More precisely, i0 is allowed to change i only where necessary, in the
sense that there is no i00 that makes do with fewer changes. This semantics follows the
possible models approach (PMA) [
Validation Tasks We now formally define the validation properties that we consider in this paper. We start with a definition of parallel – un-ordered – task nodes; some of the validation tasks will be about potential conflicts between such nodes.
Definition 5. Let G = (N ; E ; O; A) be an annotated process graph, n1; n2 2 N . We say that n1 and n2 are parallel, written n1 k n2, if there exist execution paths t1 and t2 of (N ; E ) so that n1 is executed before n2 on t1, and n2 is executed before n1 on t2.
We will show in Section 3 how parallel nodes can be detected. Note that t1 and t2 here are token executions, ignoring the semantic annotations; i.e., Definition 5 refers only to the workflow structure. We are interested in validating the following properties: Definition 6. Let G = (N ; E ; O; A) be an annotated process graph. Let n 2 NT [ fn+g. Then, n is reachable iff there exists a reachable state s so that ts(IN (n)) > 0; n is executable iff, for all reachable states s with ts(IN (n)) > 0, we have s j= pre(n). G is reachable (executable) iff all n 2 NT [ fn+g are reachable (executable).
Let n1; n2 2 NT , n1 k n2. Then, n1 has a precondition conflict with n2 if T ^ eff(n1) ^ pre(n2) is not satisfiable; n1 and n2 have an effect conflict if T ^ eff(n1) ^ eff(n2) is not satisfiable.
Consider first the notions of reachable and executable task nodes n. Reachability is important because, if n is not reachable, then it is completely useless; this certainly indicates a malfunction of the process model. As for executability, if n is not executable then the process may reach a state where n is active – it has a token on its incoming edge – but its prerequisites for execution are not given. If the process is being executed by a standard (non-semantic) engine, e.g. based on BPEL, then the implementation of n will be executed anyway, which may lead to errors. In general, the possibility to activate a task without establishing its precondition indicates that the process model does not take sufficient care of achieving the relevant conditions in all possible cases.
Reachability and executability are both temporal properties on the behaviour of the
process, and of course it may be of interest to allow arbitrary validation properties via a
suitable temporal logic (see e.g. [
Consider now the precondition and effect conflicts from Definition 6. Such conflicts indicate that the semantic annotations of different task nodes may be in conflict; n1 may jeopardise the precondition of n2, or n1 and n2 may jeopardise each other’s effects.3 If n1 and n2 are ordered with respect to each other, then this kind of conflict cannot result in ambiguities and should not be taken to be a flaw; hence Definition 6 postulates n1 k n2. Apart from that, it is debatable to some extent whether such conflicts represent flaws, or whether they are a natural phenomenon of the modelled process. Our standpoint is that they are flaws, because in a parallel execution it may happen that the conflicting nodes appear at the same time. Obviously, once parallelity is clarified, precondition and effect conflicts can be found by a simple loop over all pairs of parallel task nodes. In the remainder of the paper, we will assume that such a loop has completed successfully, i.e., without finding any conflicts. Note that reachability can be established as a side-effect of executability: 3 For illustration it is useful to consider the special case where T is empty: then, a precondition conflict means there exists l 2 eff(n1) \ :pre(n2); similarly for effect conflicts. Lemma 1. Let G = (N ; E ; O; A) be an annotated process graph without case distinctions where (N ; E ) is sound and all n 2 NT are executable. Then all n 2 NT are reachable.
We consider process graphs without case distinctions in our validation technique described in Section 3 below. We provide methods only for checking executability. With Lemma 1, once that is established, we know that reachability is also given. Note that Lemma 1 does not hold if G has case distinctions: a node may not be reachable because an edge condition on e may never become true. 2.3
An Example Process
We consider a sales order process that is inspired by the BPEL specification [
Receive Order
Production Scheduling Decide on Shipper Draft Price Calculation
Arrange Logistics Complete
Price Calculation
Production
Invoice Processing
GMP has used the depicted process successfully and without encountering any problems for years to produce and deliver to the national market. Now the company has made the decision to consider also international orders and delivery. Recently, it has received an order of 10 impulse turbines for power generation from a country that currently faces political unrest. According to German legislation such a delivery requires approval from the Bundesamt fu¨r Wirtschaft und Ausfuhrkontrolle (BAFA), i.e. the authority that controls German foreign trade. In order to deal with the complexity of international trade, GMP has decided to replace some of its production steps with services from experts. The key account manager for international clients has signed agreements with respective service providers. The new set of services including their Precondition
Postcondition orderReceived(o) productionScheduled(o,p) Activity Receive Order Production Scheduling orderReceived(o) orderApproved(o) Production productionScheduled(o,p) productionCompleted(o,p) calculationPrepared(o,c) calculationUpdated(o,c) Decide on Shipper orderReceived(o) shipperDecided(o,s) Arrange Logistics shipperDecided(o,s) calculationUpdated(o,c) calculationPrepared(o,c) shipmentApproved(o,sh) Draft Price Calculation orderReceived(o) calculationDrafted(o,c) Complete Price Calculation calculationPrepared(o,c) calculationFinalized(o,c) Invoice Processing productionCompleted(o,p)
calculationFinalized(o,c) orderCompleted(o) Purpose Definition Order status 8x : :orderReceived(x) _:orderCompleted(x) Production status 8x; y : :productionScheduled(x,y) _:productionCompleted(x,y) Calculation status 8x; y : calculationDrafted(x,y) =) calculationPrepared(x,y) 8x; y : calculationUpdated(x,y) =) calculationPrepared(x,y) 8x; y : :calculationDrafted(x,y) _:calculationFinalized(x,y) 8x; y : :calculationUpdated(x,y) _:calculationFinalized(x,y) 8x; y : :calculationPrepared(x,y) _:calculationFinalized(x,y) 8x; y : :calculationDrafted(x,y) _:calculationUpdated(x,y)
Order approval 8x; y : shipmentApproved(x,y) =) orderApproved(x) preconditions and postconditions are summarized in the top part of Table 1. In particular, the Production Scheduling, the Production, and Arrange Logistics tasks are now provided by new services that have more specialized preconditions and postconditions. Further, a domain theory, depicted in the bottom part of Table 1, has beed added, capturing some simple domain constraints that can be easily validated by stakeholders if a systems analyst translates them into natural language. Finally, Table 1 introduces thee process variables that capture the state of the involved business objects: order (o), production (p), calculation (c), shipper (s), and shipment (sh).
In a discussion with the production engineer the key account manager is embarrassed to learn that his set of services will not work for the production process of GMP, although the workflow of this process is sound. There are: Non-executable tasks: In order to cover the BAFA export approval, GMP has chosen a shipper whose Arrange Logistics service provides a postcondition of shipmentApproved if BAFA approves the delivery. Furthermore, GMP selected a Production Scheduling service that requires orderApproved as a precondition in order to block production until it is clear that the ordered goods can be exported. This alone is fine since, by the axiomatization, an order is approved if its shipment is approved. However, there is now a dependency between arranging logistics and scheduling the production, which determines the order of these two activities. Logistics must be arranged before the production is scheduled. This is not done by the process, and hence the precondition of production scheduling is not fulfilled when trying to execute it.
Precondition conflicts: The new Arrange Logistics task require the calculation c to be prepared (drafted or updated), so that it can be updated. However, Complete Price Calculation is not ordered with respect to Arrange Logistics, and if it is executed first then the status of c changes to finalized.
Effect conflicts: The new Arrange Logistics and Production services of GMP update the prize calculation, as indicated by their effect calculationUpdated. On the other hand, the parallel task Complete Price Calculation establishes the conflicting postcondition calculationFinalized. Hence, whether or not the calculation is finalized at the end of the process depends on which one of these nodes is executed last – a clearly undesirable behavior. 3
We now specify an efficient validation algorithm for a particular class of processes, namely: Definition 7. Let G = (N ; E ; O; A), O = (P ; T ), be an annotated process graph. G is basic if it contains neither loops nor case distinctions, and T is binary.
Note that our example from Section 2.3 is a basic annotated process graph. For
complexity considerations, we will in the following assume fixed arity, i.e., a fixed
upper bound on the arity of the predicates P . This is a realistic assumption because
predicate arities are typically very small in practice (e.g., in Description Logics the
maximum arity is 2). Given a process graph whose annotations mention the constants
C, and a set L of literals (such as a task node effect), in the following we denote L :=
fl 2 P [C] j T ^ L j= lg, i.e., L is the closure of L under implications in the theory
T . Since T is binary, L can be computed in polynomial time given fixed arity [
Our validation algorithm performs three steps: (1) Determine a numbering # of the
edges E so that, whenever task node n1 is ordered before task node n2 in every process
execution, then #(I N (n1)) < #(I N (n2)). (2) Using #, execute an M -propagation
algorithm that determines all pairs of parallel task nodes. (3) Determine, for each edge
e, the set of literals that are always true when e is active. In what follows, we explain
in detail only step (3). Steps (1) and (2) can be looked up in [
M is used to determine all parallel task nodes, and, with that, whether any precondition or effect conflicts arise. If so, those are indicated to the human modeller. Once the conflicts have been resolved, step (3) of our validation algorithm can be started. This step determines, for each edge e, the set of literals that is always true when e is active. The computation is based on propagation steps, updating sets of literals that are assigned to the edges. Upon completion, these literal sets are exactly the desired ones. Definition 8. Let G = (N ; E ; O; A) be a basic annotated process graph without effect conflicts, and with constants C. We define the function I0 : E 7! 2P[C] [ f?g as I0(e) = eff(n0) if e = OU T (n0), I0(e) = ? otherwise. Let I; I0 : E 7! 2P[C] [ f?g, n 2 N . We say that I0 is the propagation of I at n iff one of the following holds: 1. n 2 NP S [NXS , and I(IN (n)) 6= ?, and for all e 2 OU T (n) we have I(e) = ?, and I0 is given by I0(e) = I(IN (n)) if e 2 OU T (n), I0(e) = I(e) otherwise. 2. n 2 NP J , and for all e 2 IN (n) we have I(e) 6= ?, and I(OU T (n)) = ?, and
I0 is given by I0(e) = Se02IN(n) I(e0) if e = OU T (n), I0(e) = I(e) otherwise. 3. n 2 NXJ , and for all e 2 IN (n) we have I(e) 6= ?, and I(OU T (n)) = ?, and
I0 is given by I0(e) = Te02IN(n) I(e0) if e = OU T (n), I0(e) = I(e) otherwise. 4. n 2 NT , and I(IN (n)) 6= ?, and I(OU T (n)) = ?, and
8> eff(n) [ (I(IN (n)) n :eff(n)) e = OU T (n) I0(e) = < I(e) n :eff(n) M ##((Ie)N(n)) = 1 and I(e) 6= ? >: I(e) otherwise
If A(n) is not defined then eff(n) := ; in the above.
If I results from starting in I0, and stepping on to propagations until no more propagations exist, then we call I an I-propagation result.
Definition 8 is a little hard to read but relies on straightforward key ideas. The
definition of I0 is obvious. For split nodes (case 1), the OUT edges simply copy their
sets from the IN edge. For parallel joins (case 2), the OUT edge assumes the union
of I(e) for all IN edges e; for xor joins (case 3), the intersection is taken instead. The
handling of task nodes (case 4) is somewhat more subtle. First, although there are no
effect conflicts it may happen that a parallel node has inherited (though not established
itself, due to the postulated absence of effect conflicts) a literal which the task node
effect contradicts; hence line 2 of case 4.4 Second, we must determine how the effect of
n may affect any of the possible interpretations prior to executing n. This is non-trivial
due to the complex semantics of task executions, based on the PMA [
Due to this observation, it suffices to subtract :eff(n) in the top and middle lines of
the definition of I0(e): l does not become false in any interpretation, unless :l follows
logically from eff(n). Importantly, (*) does not hold for more general T ; see [
Note that the I-propagation algorithm ignores preconditions. This may seem odd since preconditions play an essential part in executability. The trick is as follows. Let, for any edge e, T e be the set of literals that will always be true when e is active. Then, assuming that all task nodes are executable, one can prove that T e = I (e). Now, if all nodes are executable, then, since T(e) = I (e), we have pre(n) I (IN (n)) for all n 2 NT [ fn+g. Conversely, if n 2 NT is the first node where pre(n) 6 I (IN (n)), then all of n’s predecessors are executable and we know, with the same arguments as before, that I (IN (n)) = T IN (n). Hence n is not executable. We get: Theorem 1. Let G = (N ; E ; O; A) be a basic annotated process graph without effect conflicts. There exists exactly one I-propagation result I . G is executable iff, for all n 2 NT [ fn+g, pre(n) I (IN (n)). With fixed arity, the time required to compute I is polynomial in the size of G. 4
Since the class of basic processes can be validated in polynomial time, it is interesting to determine the computational borderline of this positive result: What happens if we generalise this class? We give negative results for allowing case distinctions, and for allowing more general ontologies. It is an open question whether or not loops, or structured loops, can be dealt with efficiently. We are currently investigating this. Lemma 3. Assume an annotated process graph G = (N ; E ; O; A) that is basic except that A(e) may be defined for some e 2 E . Deciding whether G is reachable is NP-hard. Deciding whether G is executable is coNP-hard.
Lemma 4. Assume an annotated process graph G = (N ; E ; O; A) that is basic except that T is not binary. Deciding whether G is reachable is 2p-hard in general, and NPhard if T is Horn. Deciding whether G is executable is 2p-hard in general, and coNPhard if T is Horn.
Importantly, Lemma 4 holds even for propositional T . Our main result regarding the computational borderline follows directly from Lemmas 3 and 4: Theorem 2. Assume an annotated process graph G = (N ; E ; O; A). Unless P = NP, neither reachability nor executability can be decided in polynomial time if one of the following holds: G is basic except that it may contain case distinctions; G is basic except that T may involve Horn clauses.
Basic process graphs are generous in that they allow predicates with large arity, and in that they do not require the start node effect eff(n0) to be complete. One might wonder if sacrificing this generality could buy us anything. This is not the case: the proofs of Lemmas 3 and 4 do not exploit this feature.
Corollary 1. Theorem 2 holds even if predicate arity is fixed to 0, and eff(n0) is complete, i.e., if for every p 2 P[C]: either p 2 eff(n0) or :p 2 eff(n0).
It would of course be desirable to be able to not only inform the human modeller that a process is flawed, but to also suggest actual fixes for the detected bugs. This is a highly difficult task – in general, it requires an understanding of the intentions behind the process; such an understanding may not be apparent from the semantic annotations. This notwithstanding, it is interesting to observe that some bug fixes are possible based on the information determined by our algorithms from Section 3.
Assume that task node n is not executable. Assume further that we know the set of literals I(n) that are true in any state where n is activated – i.e., in case the process is basic, I(n) is the set I (IN (n)) as per Definition 8. Then we can fix this bug by inserting a new task node n0 before n, and setting pre(n0) := I(n) and eff(n0) := pre(n). SWS discovery and composition can then be used to seek an implementation of n0. In other words, we can try to automatically fill the holes in the process implementation. Note that this is only possible if our validation method answers not only “yes/no”; as is the case for our method from Section 3, the method needs to know internally which literals will be true at which points. If the validation method uses a decision procedure, like e.g. a SAT solver, for a case where answering “yes/no” is hard, then one may have to make extra arrangements to also obtain the information I(n).
If n1 and n2 have a precondition or effect conflict, then it may be possible to resolve that conflict via enforcing an ordering constraint between n1 and n2. In many cases, this can be done by inserting an additional parallel split and join between n1 and n2. Note that, for effect conflicts, there is a choice between the two possible orders. Note also that such a bug fix, and also the bug fix for executability outlined above, may introduce new bugs. Some of these issues can be overcome, e.g., by careful selection of SWS for the implementation, and/or by careful selection of ordering constraints. 6
Verification of business process models has been a field of intense research since
several years; see, e.g. [
Some other works have appeared that extend Business Process validation beyond
workflows; none of these works explores the same direction as ours, but it is worthwhile
to point out the differences. The most closely related work is [
Petri Net, and hence simplifies our notations.
than our purely conjunctive effects; on the other hand, their propagation algorithm is
exponential in the size of the process (the size of the propagated constructs multiplies
at every xor join), in stark difference to our polynomial time methods. Further, [
Another related work is [
In terms of its terminology, [
[
Another somewhat related line of work is data-flow analysis, where dependencies
are examined between the points where data is generated, and where it is consumed;
some ideas related to this are implemented in the ADEPT system [
In Semantic Business Process Management, validation techniques are needed that consider the semantic annotations to check whether a process is consistent. Such validation techniques are semantic in that they need to work with ontologies. We have devised a first formalism for this kind of validation. We have identified efficient algorithms for a class of processes, and proved that this class is maximal with respect to the expressiveness of the annotation. Our next step will be to explore our notions from a more practical perspective. In particular, we believe certain classes of loops can be addressed with variants of our current algorithms.