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 either with respect to an abstract model or with respect to 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 is represented and validated by concept satisfiability checking.
The refinement of processes is a common task in process development. 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. A key question is whether a process refinement is valid, i.e. the refined process refers to the intended behaviour of the abstract process.
We distinguish between horizontal and vertical refinement. A horizontal refinement is a transformation from an abstract to a more specific model. A vertical refinement is a transformation from a principle behaviour model of a software component to a concrete process model of business. Once a refined process model describes a concrete application process, the relationship to the original generic process is not always obvious due to a number of possibly complex refinement steps. A refinement step includes customisation, extensions and compositions of processes. Therefore it is quite difficult to validate the refinement of a process with respect to an abstract process model.
The validation of a process refinement consists of checking model constraints like execution order constraints. Modelling constraints for the refined process has to cover the constraints of the generic process behaviour and also constraints which emerged during the refinement steps.
In this paper, we use execution set semantics to analyse process refinements. This set-based formalism accounts for a comparison of the process executions of different processes. The comparison of process execution sets is then reduced to the comparison of finite sets of predecessor and successor relations which is realized by subsumption checking. We further use ALC ontologies to model processes and process constraints, concerning the execution order conditions and binding of tasks. Finally the refinement checking is reduced to concept satisfiability checking.
In Section 2 we define the problem of process refinement with its graphical syntax, semantics and mathematical foundation. The modelling of processes with the corresponding execution constraints is demonstrated in Section 3, followed by the refinement validation.
A process is a non-simple directed graph without multiple edges between two vertices. A vertex is either an activity, a gateway, a start, or an end event. As a graphical process syntax, we use the business process modelling notation (BPMN)1 due to its wide industry adoption. As an example, in Fig. 1, ( Thus in this work we consider only pairwise gateways to comply such convention. Also, we assume all the process models are valid by their own.
As a prerequisite to validating, we define the correctness of process refinement based on the execution set semantics [14]. Briefly, the execution set of a process P , denoted by ES P , is made up of all the valid paths between the Start and the End in P . ES Abstract in Fig. 1a 1c). Consequently, enumerating the execution set is infeasible.
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. The challenge is to verify whether the refinement is consistent with the more abstract horizontal and vertical processes. 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.
Renaming. Replace all activities in each execution of ES Q by their originators (function hori()). Renaming the execution set As 1b is a wrong horizontal refinement of Fig. 1a. The cause is the potentially inverted order of AB by b 1 a 2 or b 2 a 2 in Fig. 1b and that a 3 can be the last activity in Fig. 1b, whereas A must always be followed by B in Fig. 1a.
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. As
[E]}, Fig. 1b is a correct vertical refinement of both Component 1 and 2.
As enumerating the execution sets for validation is infeasible, our solution works with descriptions in ontology instead of using the execution sets themselves.
In this section, we present our solution of validating process refinement with ontologies in detail. We accomplish the transformations from the last section by reductions on the process diagram and execution sets, represent the refinement with an ontology, and validate the refinement by concept satisfiability checking.
Because the execution set may contain infinite number of executions, e.g. ES component1 , it's difficult to directly compare them. Therefore we reduce the subsumption between infinitely large execution sets into subsumption between finite predecessor and successor sets that are also obtained from the process diagram and show that the transformations on the execution sets are equivalent to transformations on the process diagrams or the predecessor and successor sets.
As we can see from ES Specif ic , the execution ordering relations between branches of a parallel gateway are implicit in the original process. In order to make them explicit, we first reduce a process diagram by the following operation:
A parallel gateway ([
, where the notation [B|P ] represents a path with B the head and a subpath P the tail.
We repeatedly apply above operation until there's no parallel gateway in the diagram. Such an iteration will always terminate due to the finite size of the process. The resulting BPMN graph is called the Execution Diagram of P , denoted by ED P (see Fig. 2). An activity a ∈ P may have multiple appearance in ED P . We use one more subscript j to differentiate them, i.e. a 2 1, a 2 2 w.r.t. a 2 . This transformation may increase the size of the process model exponentially, e.g. a pair of parallel gateways containing n branches of one activity will be transformed into a pair of exclusive gateway containing n! branches of n activity.
Obviously, given a process P , its execution set ES P is the set of all routes between Start and End in its execution diagram ED P after replacing duplicated activities with their original names. We further reduce ED P from a local perspective. For each activity appearance a in ED P , its Predecessor Set P S P (a) is the set of all the activities going to a through a direct link or a sequence containing only gateways. And its Successor Set SS P (a) is the set of all the activities going from a through a direct link or a sequence containing only gateways.
Obviously, according to the definition, for each x, y such that x ∈ P S P (a j ), y ∈ SS P (a j ), [x, a j , y] is a valid subpath of activities in ED P and thus [x, a, y] is a valid subpath of activities in P . Because the ED P is finite, P S P (a j ) and SS P (a j ) are also finite for any a j ∈ P . Follow our example, P S(a 31 ) = {a 11 } and SS(a 31 ) = {End}.
By obtaining these two sets for all the activities, the relation between two execution sets can be characterised by the following theorem: (2) For the ← direction the rhs holds and we demonstrate that ES Q ⊆ ES P follows. Consider an execution s ∈ ES Q , s = a 1 , . . . , a n . Activity a i−1 is predecessor of a i . For i = 2, . . . , n the following implication holds:
] is a subpath of some Y ∈ ES P , therefore sequentially connect the subpathes [a 1 , . . . , a n ] ∈ ES P holds. 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 original process diagrams and the predecessor and successor sets obtained from them:
-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 link their predecessors and successors directly, the resulting ES Q will be the same as the reduction of ES Q with respect to P . -Renaming can also be directly performed on the process diagram, i.e.
ES P [a → A] = ES P [a→A] . Thus, the renaming can be performed on the predecessor and successor sets as well, i.e. P S P (x)[a → A] = P S P [a→A] (x)
-Decomposition can be done on the predecessor and successor sets as well.
Particularly, ES Q ⊆ ES P , where ES Q is ES Q after decomposition of all the sequential x grouped into a single x, iff ∀a = x, P S Q (a) ⊆ P S P (a), SS Q (a) ⊆ SS P (a) and ∀x, P S Q (x) ∪ {x} ⊆ P S P (x) and SS Q (x) ∪ {x} ⊆ SS P (x). This interprets the decomposition as, any x that should be grouped, can go not only from predecessors of x, but also another appearance of x, and can go not only to successors of x, but also another appearance of x.
Thus, above analysis implies that:
-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 process diagram and obtain the predecessor and successor sets from its execution diagram, then perform Renaming and Decomposition with ontologies 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 and successors relations are described by two roles from and to, respectively. Composition of activities in horizontal refinement is described by role compose. Grounding of activities in vertical refinement is described by role groundedTo. The last two don't have essential logic difference in the problem of process refinement but have different semantics in the process model, so that we distinguish between them. Then, for a set S containing predecessors or successors, we define four operators for translations as follows: 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 → 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) For the ← direction we assume that the rhs Disjoint(x|x ∈ P ∪ Q) infers that Pr f rom (P S P (a)) Ps f rom (P S Q (a)) is satisfiable. For each activity b ∈ P S Q (a) we show that b is also in P S P (a): b ∈ P S Q (a) and Ps f rom (P S Q (a)) is satisfiable, the intersection contains the term ∃f rom.b. Since Pr f rom (P S P (a)) is satisfiable and is also the range restriction of f rom, it follows that b ∈ P S P (a). This theorem indicates that the refinement checking of processes can be reduced to the satisfiability checking of concepts in an ontology. In the following, we present the representation of horizontal refinement and vertical refinement.
Horizontal Refinement For conciseness of presentation, we always have a pre-refinement process and a post-refinement process and we refine one activity in each step (this activity may have multiple appearance after conversion to the execution diagram). We assume P the pre-refinement process, Q the post-refinement process and z the activity being refined. For each z j we define component z j ≡ ∃compose.z j . The 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 ∈ Q and hori(a) = z j , a ∃compose.z j These axioms represent the composition of activities with concept subsumptions, which realise Renaming in horizontal refinement. For example, b 11 ∃compose.B and a 31 ∃compose.A. 2. for each a ∈ Q and a is not refined from any z j a Pr f rom (P
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 the 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. 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 , a 31 ). 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 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, assume we have principle behaviour model P and a concrete process model Q, which is 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 ∈ P, ∃b ∈ Q that b is grounded to a, and vice versa. Therefore for each x j ∈ 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 ∈ Q and vert(a) = x j , a ∃groundedT o.x j These axioms represent the grounding of activities by concept subsumptions, which realise the Renaming in vertical refinement. For example, a 11 ∃groundedT o.E, b 11 ∃groundedT o.F . 2. for each a ∈ P grounded a Pr f rom (P S P (a))[x j → grounded x j ], grounded a 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 ∈ 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. For example, grounded E ∀f rom.Start, grounded E ∀to.(grounded F End). 3. for each a ∈ Q, a Ps f rom (P S Q (a)) and a Ps to (SS Q (a)),
These axioms represent the predecessor and successor sets of all the activities in the post-refinement process. For example, a 11 ∃f rom.Start, a 11 ∃to.b 11 ∃to.End. Notice that the ungrounded activities such as a 31 have been removed from the process so that End becomes a directed successor of a 11 after reduction. 4. for each x j ∈ P , Disjoint(a|a ∈ Q and vert(a) = x j )
These axioms represent the uniqueness of all the sibling activities refined from the same x j . 5. Disjoint(all the grounded x j ).
This axiom represents the uniqueness of all the activities before refinement. For example, Disjoint(Start, End, grounded E, grounded F ).
Both the horizontal and vertical refinement can be represented in DL in a linear complexity. The language is ALC. It's worth to mention that f rom and to do not need to be inverse roles because the unsatisfiability of activities is caused by the contradiction of universal and existential restrictions.
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.
Follow from the theorems and definitions presented before, the relation between the ontology O P →Q and the validity of the refinement from P to Q is characterised by the following theorem: Theorem 3. The route contains activity a in Q is invalid in the refinement from P to Q, iff O P →Q |= a ⊥.
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 3 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 3 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.
The complexity of such concept satisfiability checking is, according to the expressive power, ExpTime. we check the satisfiability of the concepts to validate the process refinement. Every unsatisfiable concept is either an invalid refinement or relating to an invalid refinement.
For While in the vertical refinement ontology, it's easy to infer that all the concepts are satisfiable. Therefore, the process model does comply to the principle behaviour models.
Helped by our analysis, the line of business manager and process architect remodel their processes (Fig. 3). Now, the execution set of Fig. 3a
After decomposition, we conclude that Fig. 3b correctly refines the process in Fig. 3a
Annotations to process models for service behaviour and interaction is described in [4,12,11]. However, process refinement and model validation is not considered. Other models use mathematical formalisms to describe and compare concurrent system behaviour. In [3] a process algebra is described in order to analyse equivalence. The analysed equivalence (trace equivalence) does not distinguish between deterministic and non-deterministic choices. Semantics for BPMN models in process algebra and process refinements are outlined in [13]. The refinement is validated with model checker.
Calculus of communication systems and transition systems is used in other works like in [7,8]. The π-calculus is a first order calculus for concurrent systems. The bisimulation (equivalence relationship between transition systems) for the π-calculus is described in [9] and in [10] higher-order process calculus is used to analyse bisimulation. Some of these approaches also apply the execution set semantics from [14], but without refinement validation.
In [5] actions and services are described in DL. Actions contain pre-and post-conditions. As inference problems, the realizability of a service, subsumption relation between services and service effect checking is analysed. Services are also described with DL in [2]. The reasoning tasks are checking of pre-and post-conditions. The focus of this work is the reasoning complexity.
The DL DLR is extended with temporal operators in [1]. Based on this extension, query containment for specified (temporal) properties is analysed. In [6] the DL ALC is extended with the temporal logics LTL and CTL. Still, neither of them considers process modelling and refinements.
In this paper, we have devised a method to checking process refinement w.r.t. execution set semantics. We restricted our solution to a commonly used subset of BPMN [15], which we may extend in the future. We perform a topological transformation of process models and translate them into ALC ontologies. The refinement checking can be reduced to concept unsatisfiability checking. In the future, we will implement and evaluate our approach, and extend it to deal with more constraints.
This work has been supported by the European Project Marrying Ontologies and Software Technologies (MOST ICT 2008-216691).