A crucial task in process management is the validation of process refinements. A process refinement is a process description in a more fine-grained representation. The refinement is with respect to either an abstract model or a component's principle behaviour model. We define process refinement based on the execution set semantics. Predecessor and successor relations of the activities are described in an ontology in which the refinement can be validated by concept satisfiability checking.
With the growing interest about applying semantic web technologies on business process modelling, many frameworks and ontological models have been proposed to facilitate a more unified semantic representation [5,6].
In model-driven software development, process models are usually created and refined on different levels of abstraction. A generic process describes the core functionality of an application. A refinement is a transformation of a process into a more specific process description which is developed for a more concrete application and based on more detailed process behaviour knowledge. In this procedure, the refined process should refer to the intended behaviour of the abstract process and satisfies behaviour constraints. To check and ensure the consistency of refinement becomes a crucial issue in process management. Currently, such consistency check is mainly done manually and few methods have been investigated to help automation. Hence the validation is error-prone, time-consuming and increases the costs during the development cycle.
In this paper, we use execution set semantics to describe two types of process refinements and present an ontological approach to represent and check them. We first apply topological transformations to reduce the refitment checking w.r.t. execution set semantics into checking of predecessors and successors of process elements. Then we encode process models into OWL DL ontologies. Finally we show that the refinement checking on the process models can be accomplished by concept ussatisfiability checking in the ontology. We implemented our approach and conducted performance evaluation on a set of randomly generated process models. Experiment results showed that, 80% of the refinement validation tasks can be performed within 1s, which is significantly faster than manually consistency checking and the correctness of the validation is guaranteed.
The rest of the paper is organised as follows: in Sec.2 we define the problem of process refinement with its graphical syntax, semantics and mathematical foundation. The representation and validation of processes with the corresponding execution constraints is demonstrated in Sec.3. In Sec. 4 we present the evaluations and in Sec.5 we review related works and conclude the paper.
In this section, we introduce preliminary knowledge about process models, process refinement w.r.t. execution set semantics and DL-based ontologies.
A process model-or short: process-is a nonsimple directed graph P = E, V without multiple edges between two vertices. As a graphical representation, we use the business process modelling notation (BPMN: http://www.bpmn.org/) due to its wide industry adoption. However, we consider a normal form of process models for the sake of this paper as opposed to the full set of partly redundant constructs in BPMN.
In our definition, vertices (V) include activities, gateways (A, G ⊆ V), and the specific vertices start and end event (v 0 , v end ∈ V). Fig. 1a shows a BPMN diagram which consists of two activities between the start and end events. exclusive and parallel gateways, respectively. We call a process normal if it does not contain parallel gateways (G = ∅)-as, for example, process model (c).
The edge set (E) is a binary relation on V. We define the predecessor and the successor functions of each v 1 ∈ V as follows: pre(v 1 ) :
These two definitions make gateways "transparent" to ordering relations. For example in Fig. 1b, SS(a1) = {b1, a2}, in Fig. 1c, P S(C) = {C, D}.
We define the semantics of a process model using the execution set semantics [18]. An execution is a proper sequence of activities (a i ∈ A): [a 1 a 2 . . . a n ]. A proper sequence is obtained by simulating token flow through a process model. A token is associated to exactly one vertex or edge. Initially, there is exactly one token, associated to the start event. Tokens can be created and consumed following the rules below. Whenever a token is created in an activity, the activity is appended to the sequence. Exactly one of the following actions is performed at a time:
-For creating a token in an activity or in the end event v 1 ∈ A ∪ {v end }, exactly one token must be consumed from the incoming edge (v 2 , v 1 ) ∈ E. -Exactly one token must be removed from an activity or from the start event v 1 ∈ A ∪ {v 0 } in order to create one token in the leaving edge (v 1 , v 2 ) ∈ E.
-For creating a token in a parallel close gateway g ∈ (G ∩ G C ), exactly one token must be consumed from every incoming edge (v, g) ∈ E. -For creating a token in an exclusive close gateway g ∈ (G ∩ G C ), exactly one token must be consumed from exactly one incoming edge (v, g) ∈ E. -Exactly one token must be removed from a close gateway g ∈ G C in order to create one token in the leaving edge (g, v) ∈ E.
- If none of the above actions can be performed, simulation has ended. The result is a proper sequence of activities-an execution. It is to be noted that each execution is finite. However, there may be an infinite number of executions for a process model. The execution set of a process model P , denoted by ES P , is the (possibly infinite) set of all proper sequences of the process model. For example, ES 1a for process (a) in Fig. 1 is {[AB]}: first A, then B (for brevity, we refer to an activity by its short name, which appears in the diagrams in parenthesis). Process (b) contains parallel gateways ( ) to express that some activities can be performed in any order: Correct Process Refinement For refinement validation we have to distinguish between horizontal and vertical refinement. A horizontal refinement is a transformation from an abstract to a more specific model which contains the decomposition of activities. A vertical refinement is a transformation from a principle behaviour model of a component to a concrete process model for an application. The validation have to account for both refinements.
Fig. 1 shows a refinement horizontally from abstract to specific while vertically complying with the components' principle behaviour. In our example scenario, Fig. 1a is drawn by a line of business manager to sketch a new hiring process. Fig. 1b is drawn by a process architect who incrementally implements the sketched process. Fig. 1c and d are the principle behaviour models of different components.
To facilitate horizontal validation, the process architect has to declare which activities of Fig. 1b implement which activity of Fig. 1a: hori(a 1 ) = hori(a 2 ) = A, hori(b 1 ) = hori(b 2 ) = hori(b 3 ) = B. For vertical validation, the process architect needs to link activities of Fig. 1b to service endpoints given in Fig. 1c and d Correct horizontal refinement. We say that a process Q is a correct horizontal refinement of a process P if ES Q ⊆ ES P after the following transformations. Correct vertical refinement. We say that a process Q is a correct vertical refinement of a process P if ES Q ⊆ ES P after the following transformations.
Renaming. Replace all activities in each execution of ES Q by their grounds (function vert()). Renaming the execution set
Reduction. Remove all activities in each execution of ES Q that do not appear in P . For our example, reduction with respect to Fig. 1c As enumerating the execution sets for validation is infeasible, our solution works with descriptions in ontology instead of using the execution sets themselves.
Description Logics and Ontologies DL-based ontologies have been widely applied as knowledge formalism for the semantic web. An ontology usually consists of a terminology box (TBox) and an assertion box (ABox). In TBox the domain is described by concepts and roles with DL constructs. In this paper, we use DL ALC. Its concepts are inductively defined by following constructs:
where is the super concept of all concepts; ⊥ means nothing; A is an atomic concept; C and D are general concepts and r is an atomic role. In DL, the subsumption between two concepts C and D is depicted as C D. If two concepts mutually subsume each other, they are equivalent, depicted by C ≡ D. When a concept can not be instantiated in any model, i.e., C ⊥, it is unsatisfiable. Two concepts are disjoint if C ¬D. In this paper we write Disjoint(C 1 , C 2 , . . . , C n ) to denote that all these concepts disjoint with one another.
In this section, we present our solution of validating process refinement in detail. We first eliminate all the parallel gateways in a process, then translate such a process into ontologies based on the predecessor and successor sets of activities, finally we show that the refinement checking can be reduced to concept unsatisfiability checking
As we can see from ES 1c , the execution ordering relations between successors of some g ∈ G O are implicit in the original process. For example, b1 and a2 does not have any explicit edge, the semantics of parallel gateway still implies that b1a2 or a2b1 must appear in some execution. In order to make such relations explicit, we eliminate all the parallel gateways while retain the execution set. Our strategy is to generate exclusive gateways to represent the executions.
Given a process P , its normal n(P ) can be obtained as follows:
1. Repeatedly replace each penning-parallel gateway g by an opening-exclusive gateway e. For each v ∈ suc(e), construct a new penning-parallel gateway g with pre(g ) = v, suc(g ) = suc(v) ∪ suc(e) \ {v} and then make suc(v) = g . 2. Remove all the edges from an opening-to a closing-parallel gateway. 3. If an opening-gateway has only one successor, remove the gateway 4. If an closing-gateway has only one predecessor, remove the gateway In step 1 direct successors of parallel gateways are "pulled" out of the gateway. Here a loop block is considered as a single successor. In this procedure, a parallel gateway with n successors is transformed into n parallel gateways with n successors but one of the successive sequence is shortened by one successor. Due to the finite length of these sequences, this replacement always terminates. Step 2 then reduces the number of successors for these remaining parallel gateways by removing "empty" edges. Step 3 and 4 finally remove the gateways. When a gateway is removed, its predecessors and successors should be directly connected.
It's obvious that this normalisation will always result in a normal process. An example of normalisation of Fig. 1b and Fig. 1d can be seen in Fig. 2.
The size of n(P ) can be exponentially large w.r.t. P in worst case: suppose P contains only a pair of parallel gateways with n sequences of one activity, then n(P ) will contains a pair of exclusive gateways with n! sequences of n activities. In normalisation, some activities will be duplicated in the process. These duplications have different predecessors (successors). We distinguish them by an additional numerical subscript. We depict such a transformed process n(P ) with distinguished activities by P . Obviously, ES P is the same as ES n(P ) after replacing all the distinguished activities by their original names. Thus, relation between two execution sets can be characterised by the following theorem:
there exists some a j ∈ A P such that P S Q (a i ) ⊆ P S P (a j ) and SS Q (a i ) ⊆ SS P (a j ).
Proof. (1) For the → direction the lhs ES Q ⊆ ES P holds. We demonstrate the subsumption for P S. For an arbitrary activity a i ∈ A Q , the activity a i is the corresponding activity before normalisation (i.e. without additional subscripts).
The activity a j is the originator or ground activity of a i in P after renaming and a j ∈ A P is the the corresponding activity after normalization of P . From the prerequisite it directly follows that the predecessors of a i ∈ A Q are predecessors of a j in Q . The subsumption of the successor set is demonstrated likewise.
(2) To prove the other direction we assume that the rhs holds. Consider an execution s ∈ ES Q we demonstrate that s ∈ ES P . For each activity a i of an arbitrary execution s ∈ ES Q the corresponding activity a i ∈ A Q is received after normalization. From the rhs it follows that there exists an activity a j ∈ A P so that each predecessor of a i is also a predecessor of a j in P and likewise for the successors of a i . After activity renaming and demonstrating for all activities of each execution of ES Q the inclusion of the lhs follows.
Therefore, we reduce the process refinement w.r.t. execution set semantics into the subsumption checking of finite predecessor and successor sets. We then show that the transformation operations of execution sets can be equivalently performed on the its process model and the predecessor and successor sets:
-Reduction on the process diagrams has the same effect on the execution sets. That means, given a component model P and a process model Q, if we reduce Q into Q by removing all the activities that do not appear in P , and connect their predecessors and successors directly, the resulting ES Q will be the same as the reduced ES Q with respect to P . -Renaming can also be directly performed on the process diagram, i.e.
ES -Decomposition can be done on the predecessor and successor sets as well.
Theorem 1 shows that the subsumption of execution sets can be reduced to subsumption of predecessor and successor sets. Decomposition means, an activity x can go from not only predecessors of x, but also another appearance of x, and can go to not only successors of x, but also another appearance of x. Any sequence of x in the execution will be decomposed.
Thus, for horizontal refinement, we can first obtain the predecessor and successor sets of activities, and then perform the Renaming and Decomposition on these sets, and then check the validity. For vertical refinement, we can first perform the Reduction on processes, then obtain the predecessor and successor sets and perform the Renaming on these sets, and finally check the validity.
In this paper, we perform Reduction directly on the a process P and obtain the predecessor and successor sets from P , then encode Renaming and Decomposition into ontology and check the validity with reasoning.
In this section we represent the predecessor and successor sets of activities with ontologies. In such ontologies, activities are represented by concepts. The predecessors/successors relations are described by two roles from and to, respectively.
On instance level, these two roles should be inverse role of each other. However this is not necessary in our solution. Composition of activities in horizontal refinement is described by role compose. Grounding of activities in vertical refinement is described by role groundedTo. To facilitate the ontology construction, four operators are defined for pre-and post-refinement process: Definition 1. : Given S a predecessors or successors set, we define four operators for translations as follows:
Pre-refinement-from operator Pr f rom (S) = ∀f rom. x∈S x Pre-refinement-to operator Pr to (S) = ∀to. y∈S y Post-refinement-from operator Ps f rom (S) = x∈S ∃f rom.
x Post-refinement-to operator Ps to (S) = y∈S ∃to.y
The effect of the above operators in refinement checking can be characterised by the following theorem:
For sake of a shorter presentation, we only prove the first part of the theorem. The proof for the second part is appropriate to the first part.
Proof. (1) We demonstrate the → direction with a proof by contraposition. The disjointness of activities holds. Supposed the rhs is unsatisfiable, i.e. Pr f rom (P S P (a)) Ps f rom (P S Q (a)) is unsatisfiable. Obviously, both concept definitions on its own are satisfiable, since Pr f rom (P S P (a)) is just a definition with one all-quantified role followed by a union of (disjoint) concepts. The concept definition behind this expression is ∀f rom. x∈P S P (a) x which restricts the range of f rom to all concepts (activities) of P S P (a). Ps f rom (P S Q (a)) is a concept intersection which only consists of existential quantifiers and the same f rom role. This definition is also satisfiable. Therefore the unsatisfiability is caused by the intersection of both definitions. In Ps f rom (P S Q (a)) the same role f rom is used and the range is restricted by Pr f rom (P S P (a)). Therefore the contradiction is caused by one activity b ∈ P S Q (a) which is not in P S P (a), but this is a contradiction to the precondition P S Q (a) ⊆ P S P (a).
(2) The ← direction can be proved similarly by contraposition.
Horizontal Refinement For conciseness of presentation, we always have a pre-refinement process P and a post-refinement process Q and we refine one activity z of P in this step. z may have multiple appearances z j in P . For each z j we define component z j ≡ ∃compose.z j . Simultaneous refinement of multiple activities can be done in a similar manner of single refinement. Then we construct an ontology O P →Q with following axioms:
1. for each activity a i ∈ A Q and hori(a) = z a i ∃compose.z j These axioms represent the composition of activities with concept subsumption, which realise Renaming in horizontal refinement. For example, b 31 ∃compose.B and a 11 ∃compose.A.
These axioms represent the predecessor and successor sets of all the unrefined activities in the pre-refinement process. Because in the post-refinement process, any activity refined from z j will be considered as a subconcept of component z j , we replace the appearance of each z j by corresponding component z j . For example, Start ∀to.component A.
These axioms represent the predecessor and successor sets of all the refined activities in the pre-refinement process. Due to the mechanism of Decomposing, we add corresponding component z j to their predecessor and successor sets, and replace the z j with component z j for the same reason as before. For example, component A ∀f rom.(Start component A). These axioms represent the uniqueness of all the sibling activities refined from the same z j . For example, Disjoint(a 11 , a 21 , a 22 , a 23 ) 6. Disjoint( all the activity in P , and all the component z j ).
This axiom represents the uniqueness of all the activities before refinement. For example, Disjoint(Start, End, A, B, component A, component B).
With the above axioms, ontology O P →Q is a representation of the horizontal refinement from P to Q by describing the predecessor and successor sets of corresponding activities with axioms.
Vertical Refinement Similar as horizontal refinement, suppose we have principle behaviour model P and a concrete process model Q, which has already been reduced w.r.t P to eliminate ungrounded activities. Any activity in Q can be grounded to some activity in P . Thus, after reduction, ∀a ∈ A P , ∃b ∈ A Q that b is grounded to a, and vice versa. Therefore for each x j ∈ A P , we define grounded x j ≡ ∃groundedT o.x j .Then we construct an ontology O P →Q with following axioms:
1. for each activity a i ∈ A Q and vert(a) = x a i ∃groundedT o.x j
These axioms represent the grounding of activities by concept subsumption, which realise the Renaming in vertical refinement. For example, a 11 ∃groundedT o.E, b 11 ∃groundedT o.F . 2. for each a i ∈ A P grounded a i Pr f rom (P S P (a i ))[x j → grounded x j ], grounded a i Pr to (SS P (a))[x j → grounded x j ], These axioms represent the predecessor and successor sets of all the activities in the pre-refinement process. Due the mechanism of Renaming we replace all the x j ∈ A P by grounded x j . Because Decomposition is not needed in vertical refinement, we stick to the original predecessor and successor sets. These axioms become the constraints on the activities in Q .
These axioms represent the predecessor and successor sets of all the activities in the post-refinement process. Notice that the ungrounded activities have been removed from the process. 4. for each x ∈ A P , Disjoint(a i |a i ∈ Q and vert(a) = x) These axioms represent the uniqueness of all the sibling activities refined from the same x. 5. Disjoint(Start, End, all the grounded x j ).
This axiom represents the uniqueness of all the activities before refinement. For example, Disjoint(Start, End, grounded C, grounded D).
With above axioms, ontology O P →Q is a representation of the refinement from P to Q by describing the predecessor and successor sets of corresponding activities with axioms.
In both horizontal and vertical refinement, the number of axioms are linear w.r.t. the size of P and Q . The language is ALC.
In ontology O P →Q , all the activities in Q satisfy the ordering relations in P by satisfying the universal restrictions and satisfy the ordering relations in Q by satisfying existential restrictions. Given the uniqueness of concepts, the inconsistency between P and Q will lead to unsatisfiability of particular concepts. The relation between the ontology O P →Q and the validity of the refinement from P to Q is characterised by the following theorems: Theorem 3. An execution path containing activity a in Q is invalid in the refinement from P to Q, iff there is some
Proof. For each a in Q the ontology O P →Q contains the axioms a Ps f rom (P S Q (a)) and a Ps to (SS Q (a)). The axioms a Pr f rom (P S Q (a)) and a Pr to (SS Q (a)) are derived from the axioms (item 1,2). Depending on the refinement either the axioms a ∃groundedT o.x j and grounded x j ≡ ∃groundedT o.x j or a ∃compose.z j and component z j ≡ ∃compose.z j are in the ontology. (1) For the → direction the lhs holds, we demonstrate that a is unsatisfiable. Since a is invalid either P S Q (a) ⊆ P S P (a) or SS Q (a) ⊆ SS P (a). From Theorem 2 it follows that either Pr f rom (P S P (a)) Ps f rom (P S Q (a)) or Pr to (SS P (a)) Ps to (SS Q (a)) is unsatisfiable and therefore a is unsatisfiable since a is subsumed. (2) The ← direction is proved by contraposition. Given a is unsatisfiable in O P →Q . Assumed a is valid in the refinement then P S Q (a) ⊆ P S P (a) and SS Q (a) ⊆ SS P (a) holds. From Theorem 2 the satisfiability of Pr to (SS P (a)), Pr f rom (P S P (a)), Ps f rom (P S Q (a)) and Ps to (SS Q (a)) follows which leads to a contradiction to the satisfiability of a.
This theorem has two implications:
1. The validity of a refinement can be checked by the satisfiability of all the name concepts in an ontology; 2. The activities represented by unsatisfiable concepts in the ontology are the source of the invalid refinement.
we check the satisfiability of the concepts to validate the process refinement. Every unsatisfiable concept is either an invalid refinement or related to an invalid refinement.
With the help of reasoning, we can easily see that Fig. 1b is an invalid horizontal refinement w.r.t. Fig. 1a According to the underlying logic, reasoning complexity is ExpTime. Helped by our analysis, the process architect remodels their process (Fig. 3). Now, the execution set of Fig. 3
We have implemented the transformation of BPMN process models and refinement information to OWL-DL ontology. In addition to the transformation, we implemented a generator which creates random, arbitrarily complex refinement scenarios. Flow correctness is ensured by constructing the process models out of block-wise patterns that can be nested. The generator is parameterized by ! ! Fig. 3. Adapted specific process for correct refinement the maximum branching factor B, the maximum length L of a pattern instance, the maximum depth of nesting N , and by the probability for loops, parallel, or exclusive flow. Most realistic appearing process diagrams were created with B = 3, L = 6, N = 3, and with a mixture of loops, parallelism, and exclusive flow to the ratio of 2 : 1 : 2.
With the given parameters, we generated 1239 refinement scenarios (197 correct, 1042 wrong) with the average and maximum number of activities in the generic and refined models printed on the left-hand side below. The generated scenarios were used to evaluate the refinement analysis on a laptop with a 2 GHz dual core CPU, 2 GB of RAM using Java v1.6 and Pellet 2.0.0. Two factors contribute to the overall complexity of the analysis:
1. Transformation to OWL-DL. As we pointed out earlier, theoretically, the complexity of the transformation can be exponential in the worst case. However, our experiments show that in many practical cases, the size of the OWL-DL knowledge base-measured by the number of axioms-remains relatively small. In particular, for 80% (90%) of the scenarios, the number of axioms was below 220 (400) (see Fig. 4). Some unusual nesting of parallel flow causes the exceptions in the diagram that have a higher number of generated axioms. Remarkably, the appearance of such cases seems to uniquely distribute over the scenarios independently of the size of the original processes due to the artificial nature of the generated scenarios. 2. OWL-DL Reasoning. The theoretical complexity of OWL-DL reasoning is exponential as well. However, our evaluation runs in Fig. 5 suggest that for the practical cases evaluated, reasoning time grows less than exponentially (less than a straight line on a logarithmic scale) compared to the number of axioms in the OWL-DL knowledge base. We separately plot the reasoning times of the correct and wrong refinements because classifying a consistent knowledge base is more expensive in general.
When comparing absolute times, reasoning consumes about two orders of magnitude more time than transformation as can be seen from the right-hand side of the table above. This determines our future research to seek improvements in the reasoning rather than in the transformation.
As for the complete run time, the above table indicates that the refinement analysis of an average scenario-with a generic process of about 6 activities and a refining process of about 17 activities-would take about 3 seconds. We consider this a simpler, yet realistic problem size.
In one of the larger evaluated scenarios, 15 generic activities were refined to 48 specific activities (for comparison: our running example contains 5 specific activities). The 63 activities in total (= 15+48) were transformed to 402 activities due to many parallel flows in that scenario. Analysis of the 765 generated axioms was performed in 18 seconds.
In the most complicated scenario of our evaluation, where a large knowledge base had to be constructed due to the heavy use of parallel gateways, total analysis time remained below 4 minutes. Although this is definitely too much for providing a real-time refinement check to process modelers, analysis took less than 1 second for 80% (≤ 220 axioms) and less than 10 seconds for 90% (≤ 400 axioms) of the examined practical cases. Compared to the manual efforts a human is required today, our approach provides a significant improvement. Furthermore, the check performed by our approach is-in contrast to the manual approach-guaranteed to be correct and thus helps to avoid costly follow-up process design errors.
There are many existing works related to our study. Some of them [17,14] come from the business process modelling and management community which investigated process property checking with model checkers.
Researchers in system transition and communication systems [13,11,10,12] also developed behaviour algebra to analyse the bisimulation, i.e. matching between processes. In some of the works, execution set semantics are also applied [18]. However, these models do not validate refinement with activity compositions.
Other models use mathematical formalisms to describe concurrent system behaviour. [3] describes concurrent system behaviour with operational semantics and denotational semantics. But the analyzed equivalence between process models does not distinguish between deterministic and non-deterministic choices.
Semantic web community contribute to this topic by providing first semantic annotations for process models such as service behaviour and interaction [4,16,15] and later automatic process generation tools [7]. However, these approaches do neither consider process refinement nor a DL based validation of relationships.
In [8] actions and services, which are a composition of actions are described in DL. Actions contain pre-and post-conditions. The focus is on a generic description of service functionality. As inference problems, the realizability of a service, subsumption relation between services and service effects checking is analyzed. Services are described similarly with DL in [2]. The reasoning tasks are checking of pre-and post-conditions of services. The main focus of this work is the reasoning complexity.
The DL DLR is extended with temporal operators in [1] for temporal conceptual modelling. In this extension, query containment for specified (temporal) properties is analyzed. In [9] the DL ALC is extended with the temporal logics LTL and CTL. Still, neither of them considers process modelling and refinements.
Our contribution is this paper includes:
1. Devising a general approach to represent and reason with process models containing parallel and exclusive gateways; 2. Applying graph-based topological approach with DL reasoning to provide automatic solution of process refinement checking; 3. Implementing and evaluating a prototype that performs process transformation and refinement checking as proposed.
In the future, there are several potential extension of this work. We will continue our implementation and evaluation to support larger and more complex process models. We will also try to extend the process representation with more expressive power. Another interesting topic is whether the process transformation itself can be automatically inferred by reasoning. We also want to integrate our refinement representation with other business process modelling ontologies.
This work has been supported by the European Project Marrying Ontologies and Software Technologies (EU ICT 2008-216691).