Work ow veri cation has been known as an important aspect of work ow management systems. Many existing approaches concentrate on ensuring the correctness of work ow processes at the syntactic level. However, these approaches are not su cient to detect errors at the semantic level. This paper contributes to ensure the semantic correctness of work ow processes. First, we propose a formal de nition of semantic constraints and an O(n3)-time algorithm for detecting redundant and con icting constraints. Second, by relying on the CPN Ontology (a representation of Coloured Petri Nets with OWL DL ontology) and sets of semantic constraints, work ow processes are semantically created. And third, we show how to check the semantic correctness of work ow processes with the SPARQL query language.
Work ows have drawn an enormous amount of attention from the research community and the industry. Over the years, work ow technology has been applied extensively to the business area. So far, various researchers have focused on process speci cation techniques [1], [2] and on conceptual models of work ow [3], [4]. However, specifying a real-world business process is mostly manual and is thus prone to human error, resulting in a considerable number of failed projects. Therefore, model quality, correctness and re-usability become very important issues. Although numerous approaches have been already developed to ensure work ow correctness at the syntactic level (e.g., avoiding deadlocks, in nite cycles, etc.). At the semantic level there may exist errors. Recently, few researches focus on checking the semantic conformance of work ow processes.
To check the semantic correctness of a model, we consider semantic constraints as domain speci c restrictions on a business process which need to be conformed during the process is executed. Let us take an example: In a process for the Order Management activity, when an order is accepted, an order con rmation must be sent out later; If no order con rmation is scheduled to be sent, or this activity is not done in the right position, a semantic error occurs.
The work in [5] provides a very useful inspiration for our work, but it does not discuss how to formulate semantic constraints and also does not mention about the control- ow perspective in process models. Our objective is to support work ow designers in generating semantically rich work ow processes which allow syntactic and semantic veri cation. In this paper, we restrict ourselves to ensure the semantic correctness of work ow processes. Our contributions are: { Giving a formal method to describe a variety of semantic constraints; { Proposing an algorithm to check redundant and con icting semantic constraints; { Developing an ontology for annotating semantic constraints and representing control ow-based business work ow processes based on that ontology; { Showing how to use the SPARQL query language [6] to check the semantic correctness of work ow processes.
This paper is organized as follows: in Section 2, we discuss related work. A short introduction to the CPN Ontology, which is de ned to represent Coloured Petri Nets (CPNs) with OWL DL, is given in Section 3. Section 4 proposes a formal de nition of semantic constraints for business processes. An algorithm used for checking redundant and con icting semantic constraints is presented. We then develop a semantic conformance-oriented ontology. In Section 5, we present the creation of correspondences between those two ontologies to develop work ow processes. These work ows enable designers to check their semantic correctness. Five semantic veri cation issues of a work ow process are introduced in Section 6. Finally, Section 7 concludes the paper with an outlook on the future research. 2
Today, software systems that automate business processes have become more and more advanced. Various researchers have paid attention to the problem of ensuring the correctness of process models. Many methods have been done in work ow veri cation. Most of them focus on the control- ow perspective, such as [7], [8], [9], [10], [11] to prevent errors (e.g., avoiding deadlocks, in nite cycles) at the syntactic level. Nevertheless, they check mainly the conformance of a work ow process based on the principle that if the constraints on data and control ow are met during execution, the work ow is correct.
Recently, a number of researches have grown beyond the scope of pure control- ow veri cation. Some approaches analyze the nal state of the whole work ow [12] or consider running processes [13], [14], [15]. In [13], semantic constraints are de ned over processes which are used to detect semantic con icts caused by violation only of dependency and mutual exclusion constraints. They presented techniques to ensure semantic correctness for single and concurrent changes at process instance level. With regard to ontological approaches, aspects of semantic correctness are considered in few researches, such as [5], [16], [17]. The approach of [17] requires both the annotation of preconditions and e ects to ensure the models are semantically correct. In [5], the SPARQL query language is used to check the semantic correctness of ontology-based process representations. Individual model elements were annotated with concepts of a formal ontology, and constraints were formalized as SPARQL queries. However, these approaches depend on the availability of an ontology and a bulky annotation of process models.
We know that the ontology-based approach for modelling business process is not a new idea. There are some works made e orts to build business work ow ontologies, such as [18], [4], [19] to support (semi-)automatic system collaboration, provide machine-readable de nitions of concepts and interpretable format. However, the issue that relates to work ow veri cation at the syntactic level is not mentioned. By extending the state-of-the-art, we use the Web Ontology Language to de ne the CPN Ontology for representing CPNs with OWL DL ontology and the semantic conformance-oriented ontology. Our ontological approach enables to create high quality and semantically rich work ow processes. 3
In this Section, we introduce the CPN Ontology [20] de ned for business processes modelled with CPNs. The purpose is to ensure the syntactic correctness of work ow processes and to facilitate business process models easy to be shared and reused.
On one hand, Coloured Petri Nets (CPNs) [21] have been developed into a full- edged language for the design, speci cation, simulation, validation and implementation of large software systems. Consequently, modelling business processes with CPNs supports work ow designers easy to verify the syntactic correctness of work ow processes [8]. On the other hand, OWL DL [22], which stands for OWL Description Logic, is equivalent to Description Logic SHOIN (D). OWL DL supports all OWL language constructs with restrictions (e.g., type separation) and provides maximum expressiveness while keeping always computational completeness and decidability. Therefore, we choose OWL DL language to represent the CPN Ontology. We believe that the combination of CPNs and OWL DL provides not only semantically rich business process de nitions but also machine-processable ones. Figure 1 depicts the core concepts of the CPN ontology.
The CPN Ontology comprises the concepts: CPNOnt de ned for all possible CPNs; Place de ned for all places; Transition de ned for all transitions; InputArc de ned for all directed arcs from places to transitions; OutputArc de ned for all directed arcs from transitions to places; Token de ned for all tokens inside places (We consider the case of one place containing no more than one token at one time); GuardFunction de ned for all transition expressions; CtrlNode de ned for occurrence condition in control nodes; ActNode de ned for occurrence activity in activity nodes, Delete and Insert de ned for all expressions in input arcs and output arcs, respectively; Attribute de ned for all CP N Ont 1hasT rans:T ransitionu 1hasP lace:P lace
u 1hasArc:(InputArc t OutputArc) P lace connectsT rans:T ransitionu 1 hasM arking:T oken T ransition connectsP lace:P laceu = 1hasGuardF unction:GuardF unction InputArc 1hasExpresion:Delete u 9hasP lace:P lace OutputArc 1hasExpression:Insert u 9hasT rans:T ransition Delete 8hasAttribute:Attribute Insert 9hasAttribute:Attribute GuardF unction 1hasAttribute:Attributeu = 1hasActivity:ActN ode t = 1hasControl:CtrlN ode T oken 1hasAttribute:Attribute Attribute 1valueAtt:V alue CtrlN ode 1valueAtt:V alue ActN ode = 1valueAtt:V alue V alue valueRef:V alue attributes of individuals); Value de ned for all subsets of I1 I2 : : : In where Ii is a set of individuals.
Properties between the concepts in the CPN Ontology are also speci ed in Figure 1. For example, the concept CP N Ont is de ned with three properties, including hasP lace, hasT rans and hasArc. It can be glossed as `The class CP N Ont is de ned as the intersection of: (i) any class having at least one property hasP lace whose value is restricted to the class P lace and; (ii) any class having at least one property hasT ransition whose value is restricted to the class T ransition and; (iii) any class having at least one property hasArc whose value is either restricted to the class InputArc or the class OutputArc'. 4
As mentioned previously, our work aims at representing work ow processes modelled with CPNs in a knowledge base. Therefore, in this Section, we focus on ensuring their quality by guaranteeing their semantic correctness. 4.1
By taking account domain experts in support of modellers at build time, a set of semantic constraints is speci ed, which then is used to develop a corresponding work ow. According to [13], there are two fundamental kinds of semantic constraints, including mutual exclusion constraints and dependency constraints. For interdependent tasks, e.g., the presence of task A indicates that task B must be included, however, task B can be executed while task A is absence. In fact, there may exist tasks that are coexistent. This refers to the coexistence constraints. Consequently, we propose three basic types: mutual exclusion constraints, dependency constraints and coexistence constraints.
Let T be a set of tasks. A semantic constraint: c = (constraintT ype; appliedT ask; relatedT ask; order; description; [Equivalence]) where: constraintT ype 2 fmExclusion; dependency; coexistenceg; appliedT ask 2 T ; relatedT ask 2 T ; order 2 fbef ore; af ter; concurrence; notSpecif iedg ; description is an annotation of the constraint; Equivalence is a set of tasks which are equivalent to task appliedT ask.
In De nition 1, the rst parameter constraintT ype denotes the type of a semantic constraint. Each value of constraintT ype refers to the relationship between the executions of the source task denoted by the second parameter appliedT ask and the target task denoted by the third parameter relatedT ask. Parameter order speci es the order between the source and target tasks in a process model. The rst four parameters are very important when de ning a semantic constraint. The fth parameter, description, is used for describing the constraint. Equivalence is an optional parameter, which contains a set of tasks (if any) being equivalent to the source task.
Let us continue the example of a process for the Order Management activity. The process is determined as follows: After receiving an order, two tasks have to do in parallel are authenticate client and check availability. If both of these tasks result \true", the order is accepted and an order con rmation is sent out. Otherwise, an order refusal is sent out. Some semantic constraints of the process are formed as follows: c1 = (dependency, authenticate client, receive request, before, receiving an order has to be performed before authenticating client, {authenticate purchaser}); c2 = (dependency, check availability, receive request, before, receiving an order has to be performed before checking availability); c3 = (coexistence, authenticate client, check availability, concurrence, client authentication and checking availability are performed in parallel); c4 = (dependency, evaluate results, authenticate client, before, evaluating the results obtained from the relevant departments); c5 = (dependency, evaluate results, receive request, before, receiving an order has to be performed before evaluating results related to the order) 4.2
Checking implicit, redundant and con icting semantic constraints A work ow process is designed based upon the speci ed semantic constraints. However, when de ning those constraints, there may occur implicit, redundant or con icting semantic constraints.
Note that a combination of two or more constraints can constitute some new constraints. This is demonstrated by the order parameter in De nition 1. As mentioned above, this parameter indicates the execution order of a source task and a target task. Consider T1, T2, T3, instances of tasks, we identify the following properties which are associative, symmetric, transitive and/or commutative presented in Table 1.
These properties are used for inferring implicit semantic constraints. As a result, detecting implicit constraints plays a crucial role in the elimination of redundant constraints. In addition, con icting constraints will lead to undesirable results. Therefore, it is necessary to resolve them before they can be applied.
Let us consider three constraints presented in Subsection 4.1, including c1; c4
and c5. According to transitivity property (
Comparing constraint c1 4 to constraint c5, their rst four values are the same, hence constraint c5 is redundant. As a result, constraint c5 has to be removed.
Because of the di erent complexity of each semantic constraint set, we need an algorithm to resolve issues related to redundancy and con ict semantic constraints. The procedure for validating the constraint set will stop as soon as it detects a couple of con icting constraints and a message is generated to notify the user. In addition, if there exist any redundant constraints, they will be removed. In our algorithm in Figure 2, the boolean function conf lict is used for checking the con ict between two constraints, e.g., it returns true if they are con icting, otherwise, it returns f alse. The function inf er is used for inferring implicit constraints. The time complexity of the algorithm is O(n3) where n is the number of semantic constraints. To provide a representation of semantic constraints related to process elements, in next Subsection, we will describe an approach for constructing a semantic conformance-oriented ontology. 4.3
Development of a Semantic conformance-oriented Ontology Our work aims at representing processes modelled with CPNs in a knowledge base. Therefore, to provide a representation of semantic constraints related to process elements, we develop an approach for constructing a new ontology. This ontology is oriented to semantic conformity checking in work ow processes. We focus on formalizing the concepts/relations corresponding to the knowledge that is required by model elements.
The following keystones to transform a set of semantic constraints into an OWL DL ontology:
Each semantic constraint c is mapped to an instance of owl : Class. appliedT ask and relatedT ask are mapped to two instances of owl : Class. The rdf s : subClassOf property is used to state that these classes is a subclass of the constraint class.
Each value of constraitT ype or order is de ned as an instance of the built-in OWL class owl : ObjectP roperty. description is de ned as an instance of the built-in OWL class owl : Datatype P roperty; Each value in the set Equivalence is mapped to an instance of owl : Class. The built-in property owl : equivalentClass is used to link every class description of these classes to the class description of appliedT ask.
In the upcoming Section, we will discuss about the integration of a semantic conformance-oriented ontology (domain knowledge) and the CPN Ontology to create work ow processes. 5
We rely on ontology mapping techniques for matching semantics between ontologies, i.e., the CPN Ontology and Domain Ontology (a semantic conformanceoriented ontology). In our case, the articulation of two ontologies are used not only for creating semantically work ow processes, but also for verifying their correctness.
We now de ne our use of the term \mapping": Consider two ontologies, O1 and O2. Mapping of one ontology with another is de ned as bringing ontologies into mutual agreement in order to make them consistent and coherent. It means that for a concept or a relation in ontology O1, we try to nd the same intended meaning in ontology O2; For an instance in ontology O1, we nd the same instance in ontology O2.
De nition 2 (Mapping related to the bef ore property).
We de ne a mapping for all instances IC of a semantic constraint in which the order between the instance of class appliedT ask, named taska, and the instance of class relatedT ask, named taskb, is indicated by the object property bef ore. The type of instance IC is either dependency or coexistence. A set of correspondences is determined as follows:
Each instance of class appliedT ask or relatedT ask is mapped into an instance of class T ransition (expressing activity node).
There exists a ring sequence t1t2 : : : tn, where t1; tn are the instances of class T ransition corresponding to instances taska and tb respectively, ta = t1, tb = tn n 2.
De nition 3 (Mapping related to the concurrence property).
We de ne a mapping for all instances IC of a semantic constraint in which the order between the instance of class appliedT ask, named taska, and the instance of class relatedT ask, named taskb, is indicated by the object property concurrence. The type of instance IC is coexistence. A set of correspondences is determined as follows:
Each instance of class appliedT ask or relatedT ask is mapped into an instance of class T ransition (expressing activity node).
Two instances of class transitions which correspond to instance taska and instance taskb can be enabled at the same time.
It is important to underline that object property bef ore is the symmetrical property of object property af ter. Consequently, we do not de ne a mapping related to the af ter property.
By continuing the process schema for the order management activity in Section 4, Figure 3 shows the mapping of some instances between two onotologies, CPN Ontology and Semantic Conformance-oriented Ontology.
We have introduced the formal de nition of semantic constraints and illustrated how to model a work ow process with CPNs based on speci ed semantic constraints. Note that concrete work ow processes are represented in RDF syntax. Moreover, to develop or modify a work ow process, manipulation operations [20] (e.g., inserting a new element) are required. Therefore, it is necessary to verify work ow processes at design time before they are put into use. 6
By using the algorithm presented in Section 4, the sets of speci ed semantic constraints are checked redundant and con icting. Hence, we here pay attention to the research question relating to semantic veri cation: Is the behavior of the individual activities satis ed and conformed with the control ow? To answer this question, we address the following semantic veri cation issues: Are there activities whose occurrences are mutual exclusion, but that may be executed in parallel or in sequence? Are there activities whose executions are interdependent, but that may be carried out in choice or in parallel? Are there activities whose occurrences are coexistent, but that may be executed in choice? Are there any couples of activities whose order executions are de ned as one before the other, but that may be executed in the opposite? Are there any couples of activities whose order executions are de ned as one after the other, but that may be executed in the opposite order? Because concrete work ows are stored in RDF syntax, we rely on the CORESE [23] semantic search engine for answering SPARQL queries asked against an RDF knowledge base. We initiate SPARQL queries to verify whether work ow processes contain semantic errors or not. SELECT query form is chosen for this work. After a SELECT keyword, the variables are listed that contain the return values. And in the WHERE clause, one or more graph patterns can be speci ed to describe the desired result.
The following query1 relating to the third veri cation issue is used to query if the model contains `any pairs of activities whose occurrences are coexistence but that may be executed in choice'. The properties h : coexistence and h : concurrence de ned in the rst ontology indicate the semantic constraint between activities ?t1 and ?t2. On the other hand, the other properties de ned in the second ontology which represent these activities restricted to the control ow perspective. By applying this query to the work ow example depicted in Figure 3, the result is empty.
The sample query does not only demonstrate that the SPARQL query language is able to check the semantic correctness of work ow processes, but also the usage of terminological background knowledge provided by the semantic conformance-oriented ontology and CPN Ontology. 1 The pre x is assumed as:
P REF IXh :< http : ==www:semanticweb:org=CP N W F # >
Moreover, by representing CPNs-based business processes with OWL DL ontology we can also verify the soundness of models. This means that we can check syntactic errors (for example, deadlocks, in nite cycles and missing synchronization, etc.) by the SPARQL query language.
SELECT ?t1 ?t2 WHERE { ?t1 rdf:type h:Transition ?t2 rdf:type h:Transition ?t3 rdf:type h:Xor-split ?t4 rdf:type h:Xor-join ?t1 h:coexistence ?t2 ?t2 h:concurrence ?t1 ?t3 h:connectsPlace/h:connectsTrans ?t1 ?t3 h:connectsPlace/h:connectsTrans ?t2 ?t1 h:connectsPlace/h:connectsTrans ?t4 ?t2 h:connectsPlace/h:connectsTrans ?t4 FILTER (?t1!=?t2) } 7
This paper presents a formal method for describing semantic constraints that are used to generate work ow processes. First, we propose a formal de nition of semantic constraints. Then we describe an algorithm for detecting redundant and con icting semantic constraints. To integrate the domain knowledge used for annotating the process elements, we develop a semantic conformance-oriented ontology. This ontology is then matched with the CPN Ontology (a representation of CPNs with OWL DL). The mapping is to enable work ow processes which can be veri ed at the semantic level and also syntactic level. Furthermore, we demonstrate that the SPARQL query language is able to check the correctness of concrete work ow processes represented in RDF syntax. This ensures error-free work ow processes at build-time.
We know that verifying work ow processes at build-time is not enough to guarantee work ows can be executed correctly. The correctness of work ow execution must also be checked. Therefore, in future work, we plan to develop a run-time environment for validating concrete work ows. 3. Barros, A.P., ter Hofstede, A.H.M., Proper, H.A.: Essential principles for work ow modelling e ectiveness. In: PACIS. (1997) 15 4. Koschmider, A., Oberweis, A.: Ontology based business process description. In:
EMOI-INTEROP, Springer (2005) 321{333
5. Fellmann, M., Thomas, O., Busch, B.: A query-driven approach for checking the
semantic correctness of ontology-based process representations. In: BIS. (2011)
62{73
6. W3C: Sparql 1.1 query language. http://www.w3.org/TR/sparql11-query/ (March
2013) W3C Recommendation.
7. van der Aalst, W.M.P.: Veri cation of work ow nets. In: ICATPN. (1997) 407{426
8. Verbeek, H., Basten, T., van der Aalst, W.: Diagnosing work ow processes using
wo an. The computer journal 44 (1999) 246{279
9. Bi, H.H., Zhao, J.L.: Applying propositional logic to work ow veri cation.
Information Technology and Management 5(3-4) (2004) 293{318
10. Wainer, J.: Logic representation of processes in work activity coordination. In:
Proceedings of the 2000 ACM Symposium on Applied Computing - Volume 1. SAC
'00, New York, NY, USA, ACM (2000) 203{209
11. Sadiq, W., Maria, Orlowska, E.: Analyzing process models using graph reduction
techniques. Information Systems 25 (2000) 117{134
12. Lu, S., Bernstein, A.J., Lewis, P.M.: Automatic work ow veri cation and
generation. Theor. Comput. Sci. 353(
Eng. Technol. 3(4) (2007) 374{396
19. Sebastian, A., Tudorache, T., Noy, N.F., Musen, M.A.: Customizable work ow
support for collaborative ontology development. In: 4th International Workshop
on Semantic Web Enabled Software Engineering (SWESE) at ISWC 2008. (2008)
20. Nguyen, T.H.H., Le-Thanh, N.: An ontology-enabled approach for modelling
business processes. In: Beyond Databases, Architectures, and Structures. Volume 424
of Communications in Computer and Information Science. Springer International
Publishing (2014) 139{147
21. Kristensen, L.M., Christensen, S., Jensen, K.: The practitioner's guide to coloured
petri nets. STTT 2(