# Verifying Service Choreography Model Based on Description Logic.

1. IntroductionWeb service technology has been popularly applied due to its power of interoperation, which allows various applications to run on heterogeneous platforms. Standards for web service composition cover two different levels of view: choreography and orchestration [1,2]. The choreography view describes the interactions between services from a global perspective, while the orchestration view focuses on the interactions between one party and others. The web service choreography description language (WS-CDL) [3] is an XML-based language for the description of peer-to-peer collaborations of participants from a global viewpoint. However, WS-CDL is a declarative language and the specified concepts are weakly constrained. It lacks a formal system to accurately express the semantics of service behaviors and verify the correctness of a service choreography model. As a result, the built models may suffer from the problem of inconsistency, conflict, and realizability.

A number of approaches are suggested for formally modeling and verifying web services composition. Xiao et al. [4] proposed a process algebra called probabilistic priced process algebra (PPPA) for modeling and analyzing web service composition from both functionality and nonfunctionality, such as reliability and performance. Moreover, they provided a united method based on PPPA to model and analyze both functionality and QoS of web service composition. Cambronero et al. [5] presented an approach to validation and verification of web services choreographies and more specifically for composite web services systems with timing restrictions. They defined operational semantics for a relevant subset of WS-CDL and then provided a translation of the considered subset into a network of timed automata for the validation and verification using the UPPAAL tool. Zhou et al. [6] put forward an approach to testing WS-CDL programs automatically. The dynamic symbolic execution technique was used to generate test inputs, and assertions are treated as the test oracles. An engine that can simulate WS-CDL is used to execute the WS-CDL programs during symbolic execution. Besson et al. [7] adapted the automated testing techniques used by the Agile Software Development community to the SOA context to enable test-driven development of choreographies. They present the first step in that direction, a software prototype composed of ad hoc automated test case scripts for testing a web service choreography. Gu et al. [8,9] originally advocated for a formal modeling framework, called Abstract WS-CDL. This includes grammar, congruence relations, and operational semantics. They defined a set of mappings of the Abstract WS-CDL global model to the Pi calculus-based local model and subsequently suggested a set of deductive reasoning rules of state reachability and terminability.

One of the crucial questions in choreography-based development is to check the realizability and conformance properties. Halle and Bultan [10] proposed a novel algorithm for deciding realizability by computing a finite state model that keeps track of the information about the global state of a conversation protocol that each peer can deduce from the messages it sends and receives. McNeile [11] provided a new technique that uses compositions of partial descriptions to define a choreography, and he demonstrated that realizability of a choreography defined as a composition only needs to be established individually for the components of the composition. Basu et al. [12] gave necessary and sufficient conditions for realizability of choreographies and implemented the proposed realizability check on three granularities: (1) web service choreographies, (2) singularity OS channel contracts, and (3) UML collaboration (communication) diagrams. Yeung [13] put forward a formal approach to web service composition and conformance verification based on WS-CDL and WS-BPEL. The main contributions included a precise notion of choreography conformance upon which verification is based and support for the complementary use of visual modeling (e.g., UML) and standard [WS.sup.-*] notations in composition.

We argue that checking the realizability and conformance properties should be approached in two ways. One is to check the completeness and consistency of a choreography specification to guarantee there are no logical conflicts in the specification. The other is to check whether the specified choreography behaves in a correct way or whether the system functions well to complete its jobs. Having investigated the recent research results, we found that most of them addressed only one side rather than both.

To solve the problem above, we propose an approach of choreography model verification based on Description Logic, or CMV-DL. A service choreography modeling framework is provided to support UML-based modeling. The metamodel of service choreography extends the WS-CDL specification. Two algorithms are given to transform the UML-based service choreography model into the DL-based ontology through which the verification can be made using a DL reasoner.

To enable automatic verification, we introduce Description Logic (DL) [14] to formalize the choreography model and define a set of rules and constraints for verification. DL is a knowledge representation language and is a decidable subset of first-order predicate logic. It contains a set of basic concept constructors, such as concept consumption ([subset not equal to]) and universal constraint ([for all]). As a subset of DL, SHOIN(D) [15] is the logical basis of web ontology language (OWL) [16]. It is powerful in knowledge description ability, reasoning decidability, and knowledge reusability and more importantly there are available supporting reasoners such Pellet [17] and Racer.

The rest of the paper is organized as follows. Section 2 introduces the service choreography modeling framework, highlighting the metamodel of service choreography. Section 3 discusses CMV-DL further on model verification mechanism and UML-DL conversion and introduces the deductive reasoning rules specified in Semantic Web Rule Language (SWRL) [18]. Section 4 provides a case study to show the potential usage of CMV-DL. Section 5 investigates the related work and draws a comparison between CMV-DL and other choreography verification methods. The final section brings a conclusion and foresees our future work.

2. Service Choreography Modeling Framework

According to the OMG's four-layered metamodel architecture, UML can be extended by defining new stereotypes at metamodel level (M2) [19] and thus becomes a domain-specific language. The modeling framework for service choreography is accordingly defined in two levels, as shown in Figure 1. The metamodel of service choreography is built by extending the concepts of WS-CDL to provide the syntax and semantics for visually presenting a choreography and define a set of domain rules for model checking. The application model specifies the concepts of service choreography of an application (or a system) by instantiating the concepts of the metamodel.

2.1. Metamodel of Service Choreography. To build the metamodel of service choreography, we define the main concepts of service choreography by referring to the WS-CDL specification.

Definition 1 (session (S)). A session is composed of a set of basic interactive activities which are performed by one or more participants in order to complete a specific function. Sessions can be denoted as a four-tuple structure: S = <N, Act, Ro, Pr>, where N is the name, Act refers to the activities that realize this specific function, Ro is a set of the roles that participate in the activities, and Pr is a set of the preconditions for carrying out this session.

Definition 2 (choreography (Cho)). A choreography defines the collaboration contracts between the participants and the interoperations of cross-system behaviors. It can be denoted as a three-tuple structure: Cho = <N, Ro, S>, where N is the name, Ro is a set of the roles that participate in the interoperations, and S represents a set of sessions to be executed in the interoperation processes.

Definition 3 (metamodel). The metamodel of service choreography defines the syntax and semantics for visually presenting a choreography and provides a set of domain rules for checking the correctness properties of a choreography model. It is composed of three parts: {MetaConcept, MetaRelation, DomainRule), where MetaConcept and MetaRelation are sets of metaconcepts and metarelations which are defined by inheriting the counterpart concepts from the WS-CDL specification. The core elements of the metamodel are shown in Figure 2.

2.1.1. MetaConcept. MetaConcept is a finite set of metaconcepts that originate from WS-CDL but are not limited to it. New concepts, such as Session, AtomicSession, and CompoundSession, are extended for the purpose of formal modeling and verification. Table 1 provides detailed definitions and descriptions of the metaconcepts.

The concept activity can be divided into two kinds: BasicActivity (Abas) and StructuralActivity (Astr):

Act := Abas | Astr (1)

Abas is defined as

Abas := NoAction | SilentAction | Interaction | Assign |

Perform (2)

Astr is used to describe a compound activity in following syntax and semantics:

[mathematical expression not reproducible] (3)

The structure of a compound activity appears either in workunit pattern or in control-flow pattern. The workunit structure is defined in WS-CDL by three substructures. The condition structure is expressed as [p]Act. The repeat structure is expressed as [p] * Act. A workunit structure is expressed as [[p.sub.g]][[p.sub.rep]] * Act, which means that the activity will be blocked until the precondition [p.sub.g] is evaluated to be "true"; that is, the activity is triggered by the precondition. If Act terminates successfully and the repetition condition [p.sub.rep] is "true," the workunit will repeat; otherwise, it will finish. A control-flow structure is defined as any combination of sequentially executed activities [Act.sub.1] x [Act.sub.2], parallel executed activities [Act.sub.1] [parallel] [Act.sub.2], nondeterministically executed activities [Act.sub.1]T[Act.sub.2], or selectively executed activities [[p.sub.1]][Act.sub.1] + [[p.sub.2]][Act.sub.2].

The concept session can also be divided into two kinds: AtomicSession ([S.sub.atom]) and CompoundSession ([S.sub.com]):

S := [S.sub.atom] | [S.sub.com] (4)

An atomic session may appear in any form of the following:

[mathematical expression not reproducible] (5)

[S.sub.no] describes that the role Ro does not perform any operation; [S.sub.silent] means that Ro performs an internal silent action [tau]; [S.sub.assign] describes an assignment operation that the value e is assigned to the variable Ro x x; [S.sub.req] describes a request interaction from [Ro.sub.1] to [Ro.sub.2] through Ch@[Ro.sub.2], where the request message is sent from [Ro.sub.1] x x to [Ro.sub.2] x y; [S.sub.resp] describes a response interaction; [S.sub.req-resp] describes request-response interaction; [S.sub.perform] describes invoking operation between sessions; and NULL denotes the termination state of a session.

Two or more atomic sessions may be combined with one another by structural connectors to become a compound session [S.sub.com]. The combination follows the following syntax and semantics:

[mathematical expression not reproducible] (6)

[S.sub.parallel] describes two parallel executed sessions; [S.sub.sequence] describes two sequentially executed sessions where [S.sub.1] is the predecessor and [S.sub.2] is the successor; [S.sub.choice] describes two selectively executed sessions that either [S.sub.1] or [S.sub.2] will be executed depending on whether the precondition [p.sub.1] or [p.sub.2] is met; [S.sub.workunit] describes a repeatedly executed session, where S is triggered by the precondition [p.sub.g] and it will be repeatedly executed until [p.sub.rep] becomes "false."

2.1.2. MetaRelation. MetaRelation is a finite set of semantic associations between the metaconcepts appearing in Table 1. It inherits the concepts of semantic verbs, such as Support, Perform, and Depend, from WS-CDL and is supplemented by some new relations such as SessionDeduction, Congruence, and Sequence, to enable comprehensive model checking.

Table 2 provides a set of core metarelations accompanied with their formal semantics specified in DL. The universal constraint V is a DL symbol interpreted by [([for all]R x C).sup.I] = {a [member of] [[DELTA].sup.I] | [for all]b((a, b) [member of] [R.sup.I] [right arrow] b [member of] [C.sup.I])}, where C is a set of metaconcepts, R is a set of metarelations, and [[DELTA].sup.I] denotes nonempty set of discourse domains.

Definition 4 (SessionDeduction). SessionDeduction is defined by a labeled transition system: [mathematical expression not reproducible], meaning that the session S will become S' in the future when the precondition p becomes true and the atomic session a of S has been executed. SessionDeduction is defined for state reachability reasoning.

Definition 5 (congruence). If the two sessions S and S' behave exactly in same way, there is a congruence relation between them, marked with the symbol [equivalent to]. The conditions of congruence are listed as follows:

[mathematical expression not reproducible] (7)

Definitions of MetaConcept and MetaRelation provide the syntax and semantics for modeling service choreography. In the subsequent sections, we will discuss the operational semantics for session evolution and the deductive domain rules for checking the properties of consistency, completeness, and state reachability of a service choreography model.

2.1.3. DomainRule. Domain rules are description of constraints for specific domains [20]. DomainRule is a set of rules defined upon the metamodel, providing overall constraints that need to be held by all concepts and relations in the service choreography model.

Domain rules of service choreography can be classified into three categories: consistency, completeness, and deductive reasoning. They are not limited to what we give in the following. They may be continuously enriched and improved as applied.

Definition 6 (consistency). A service choreography model is consistent provided that (1) the application model is built consistent with the metamodel and (2) there is not any conflict among the concepts of the application model. A typical set of consistency rules are defined below.

(i) [R.sub.con1]: if there is a metarelation R that associates the metaconcept [C.sub.i] with [C.sub.j] ([C.sub.i] [subset not equal to] [for all]R x [C.sub.j]) in the metamodel and r is instance of R that associates the application concept [c.sub.i] with [c.sub.j] in the application model, then [c.sub.i] must be an instance of [C.sub.i] and [c.sub.j] must be an instance of [C.sub.j].

(ii) [R.sub.con2]: no more than one relation of Sequence, Parallel, Choice, or WorkUnit is allowed to associate a pair of sessions.

(iii) [R.sub.con3]: if two sessions are associated with the relations SessionDeduction([S.sub.i], [S.sub.j]) and Congruence([S.sub.i], [S.sub.j]) (i [not equal to] i) at the same time, the atomic session [S.sub.atom] associated with [S.sub.i] by the Executing relation must be in type of [S.sub.no], [S.sub.silent], or NULL.

(iv) [R.sub.con4]: if two sessions are associated with the relation Executing([S.sub.i], [S.sub.j]) (i [not equal to] j), [S.sub.j] must be an atomic session, that is, [S.sub.j] - [S.sub.atom].

(v) [R.sub.con5]: if two associated application concepts a and b are declared in the application model, there must be a metaconcept C and a metarelation R that satisfy a : C and (a, b) - R.

(vi) [R.sub.con6]: the two relations Sequence([S.sub.i], [S.sub.j]) and Sequence([S.sub.j], [S.sub.i]) i [not equal to] j, are allowed to exist at the same time.

The WS-CDL specification includes many clauses stated with the keywords such as MUST/MUSTNOT, SHOULD/SHOULDNOT, and SHALL/SHALLNOT. Those clauses may relate to the consistency and completeness constraints. For example, "a Choreography MUST contain one or more sessions," from which we can formally define a rule Choreography [subset not equal to][greater than or equal to] 1 Contain.Session in DL. The DL expression [greater than or equal to] nR x C, used for constraining a relation, is interpreted by [([greater than or equal to]nR x C).sup.1] = {a [member of] [[DELTA].sup.I] | #{b [member of] [[DELTA].sup.I] | (a, b) [member of] [R.sup.I] [conjunction] [member of] [C.sup.I]} [greater than or equal to] n}, where R is a metarelation and C is a metaconcept, and [[DELTA].sup.I] denotes nonempty set of discourse domains.

Definition 7 (completeness). A service choreography model is complete provided that the number of the relations in the application model satisfies the multiplicity constraint of the corresponding metarelation in the metamodel. A typical set of completeness rules are defined below, according to the WS-CDL specification:

(i) [R.sub.com1]: Role [subset not equal to][greater than or equal to] 1 Belong_to.Participant [??] Role [subset not equal to][less than or equal to] 1 Belong_to.Participant.

(ii) [R.sub.com2]: Session [subset not equal to][greater than or equal to] 1 Support.Activity.

(iii) [R.sub.com3]: Channel [subset not equal to][greater than or equal to] 2 Link.Role [??] Channel [subset not equal to][less than or equal to] 2 Link.Role.

(iv) [R.sub.com4]: Interaction [subset not equal to][greater than or equal to] 1 Depand.Channel.

(v) [R.sub.com5]: Participant [subset not equal to][greater than or equal to] 1 Implement.Role.

(vi) [R.sub.com6]: Choreography [subset not equal to][greater than or equal to] 1 Contain.Session.

(vii) [R.sub.com7]: Interface [subset not equal to][greater than or equal to] 1 Bind.Role [??] Interface [subset not equal to][less than or equal to] 1 Bind.Role.

Deductive reasoning rules relate to operational semantics that describes the evolution of a session. They are used to verify the state reachability of service choreography. Every deductive reasoning rule is a Horn clause in the following form: IF {antecedent) THEN {consequent), where the antecedent is a conjunction of one or more clauses and the consequent is an assertion of facts.

The relation SessionDeduction defines deduction of session evolution. If the precondition p holds and the session S executes an atomic session a making S become the session S', then S is deduced to S'. In particular, the two sessions can be identified by two states, before and after evolution.

Choreography model checking may concern two kinds of state. One is the session state that defines whether a session can normally end and successfully complete its job. The other is the application state that defines whether an application that is running on one or more sessions can normally end. As a session will never end until all atomic sessions end, the state space of a session is determined by all possible states of the atomic sessions. Similarly, the state space of an application is determined by all possible states of the sessions.

Definition 8 (state reachability). A state (session state) is reachable provided that there is an evolving session which can be identified by the state and which can be deduced from its ancestor in its initial state.

Inference 1. If the termination states of an application described by a choreography model are reachable, that is, the termination sessions (denoted as NULL) can be deduced from the initial sessions, then all states of the application are reachable and the choreography models are thereby proven correct.

The basic deductive reasoning rules are listed as follows:

(i) [mathematical expression not reproducible] (8)

(ii) [mathematical expression not reproducible] (9)

(iii) [mathematical expression not reproducible] (10)

(iv) [mathematical expression not reproducible] (11)

(v) [mathematical expression not reproducible] (12)

(vi) [mathematical expression not reproducible] (13)

(vii) [mathematical expression not reproducible] (14)

(viii) [mathematical expression not reproducible] (15)

(ix) [mathematical expression not reproducible] (16)

[R.sub.atom] is the rule that holds the indivisibility of an atomic session. [R.sub.struct] is the rule that keeps the congruence in session deduction. [R.sub.seq1] and [R.sub.seq2] are the deduction rules for the sequence sessions. [R.sub.parallel] is the deduction rule for parallel session that two sessions are parallel executed and one of them evolves. [R.sub.choice] is the deduction rule for the choice session that if the precondition is true and the atomic session is executed, one of the two sessions will evolve. [R.sub.nonblock] is the deduction rule for the workunit that if the precondition is false and [[p.sub.g]][[p.sub.rep]] * S works in nonblocking mode, the workunit will be skipped. [R.sub.norepeat] is the deduction rule for the workunit that if [p.sub.g] is "true" and [p.sub.rep] is "false" S will become S' and the workunit will become S' after execution of a. [R.sub.repeat] is the deduction rule for the workunit that if both [p.sub.g] and [p.sub.rep] are "true" S will become S' and the workunit will become S' x [[p.sub.rep]] * S after execution of a, where [[p.sub.rep]] * S means if [p.sub.rep] is "true" then S will be iteratively executed.

2.2. Application Model of Service Choreography. The metamodel gives a formal definition of the metaconcepts and relations of service choreography and provides fundamental semantics for service choreography description. An application model, an instantiation of the metaconcept model, gives a UML-compliant description and representation of service choreography. To build the model, software engineers would start with analysis of the objectives to be achieved in the choreography and then describe the roles that participants implement, the activities that the roles perform, and the session execution patterns.

Definition 9 (application model of service choreography). The application model of service choreography formally describes the design of service choreography for a distributed application in a UML-compliant representation within the constraint of the metamodel. It comprises three parts: {.AppConcept, AppRelation, AppFunction).

AppConcept is a finite set of application concepts which are defined by instantiating the metaconcepts of the metamodel. AppRelation is a finite set of application relations which are defined by instantiating the metarelations of the metamodel. AppFunction is a set of functions that map AppConcept to MetaConcept or AppRelation to MetaRelation in order to trace the types of application concepts and relations in the metamodel. For example, Buyer is an AppConcept and Role is the corresponding MetaConcept, and thus the function is built as follows: AppFunction(Buyer) = Role.

The application model, if built with a universal UML tool, may suffer from the problems of inconsistency, incompleteness, and unreachable states, as mentioned in Section 2.1.3. The next section will discuss the technique of transforming the UML-based model into DL ontology to verify the correctness of the model with the help of a popular reasoner.

3. Model Transformation and Verification

UML is a semiformal specification language and it does not by itself support logic inference for model checking. A popular solution is to use OCL (Object Constraint Language), a subset of UML for defining domain constraints in first-order predicate logic for model checking. Unfortunately, it is well known that the full expressiveness of OCL may lead to undecidability of reasoning [21]. As a result, the existing methods have to either limit the UML/OCL constructs or decrease the level of automation or balance between the two.

To solve the problem, we suggest using SHOIN(D), the subsystem of DL, to formalize the models. DL is proven powerful in expressibility and decidability for knowledge engineering and allows for making use of some handy reasoning engines, such as Pellet and Racer. But engineers may worry about the fact that it is hard to learn a formal language, hoping that the formal language would be hidden by a software tool.

This section will discuss the algorithms for model transformation, the mechanism of model verification based on SHOIN(D), and the way of implementing prototype.

3.1. Mechanism for Service Choreography Model Verification Based on SHOIN(D). In the early stage of our research, we obtained some meaningful achievements in DL-based reasoning. Dong et al. [22,23] checked the C4ISR (Command, Control, Communication, Computer, Intelligence, Surveillance, and Reconnaissance) domain models to guarantee the consistency and completeness through converting the UML models into the Description Logic ontology and making use of inference engine Pellet. He et al. [24] presented a method of UML behavioral model verification based on Description Logic system. He et al. transformed UML behavioral models to OWL DL ontology, and hence model consistency can be verified with DL supporting reasoner. Zhang [25] tried to transform the service-oriented application models to OWL DL ontology. Based on the above research, we present, as shown in Figure 3, a mechanism for service choreography model verification based on SHOIN(D).

The principle of conversion and verification is as follows: (1) convert the metaconcepts of service choreography model and domain rules into the axiom sets in SHOIN(D) Tbox and the application concept model into the assertion sets in SHOIN(D) Abox; (2) verify the consistency, completeness, and state reachability with the help of a reasoning engine like Pellet that supports logical reasoning through the SHOIN(D) ontology. The automatic conversion can be realized by Algorithms 1 and 2.

Step (1) initializes Tbox and Abox. Steps (2)-(10) convert the metaconcepts and relations of the metaconcept model into axiom sets in Tbox. Steps (11)-(17) add multiplicity constraints of metarelations as axiom sets in Tbox. Subsequently, steps (18)-(24) convert application concepts and relations of the application model into assertion sets in Abox. For a more detailed explanation for each step, refer to our previous work in [22,24]. Our previous work [23] showed that the conversion is correct and there is no semantics loss.

The domain rules need to be transformed into axiom sets in Tbox. The consistency and completeness rules are specified in DL and can be added to Tbox through steps (11)-(17), while the deductive reasoning rules need to be specified in SWRL. SWRL combines RuleML and OWL DL. It is popularly applied for formal representation of semantic rules and knowledge-based reasoning, supported by the algorithm Tableau [15].

Algorithm 2 is provided to convert the deductive reasoning rules in the choreography model into the formally specified rules in SWRL.

The concepts and relations appearing in the prerequisite of the deductive reasoning rules are converted to Horn clauses that combine to form the antecedent of SWRL rules, and the concepts and relations appearing in the conclusion are converted to Horn clauses that combine to form the consequent of SWRL rules.

For example, the deductive reasoning rules [R.sub.atom] and [R.sub.struct] are converted into following SWRL expressions:

[mathematical expression not reproducible] (17)

3.2. Prototype Implementation. Algorithms 1 and 2 have been realized and integrated into our requirement analysis tool, the so-called ontology-based requirements elicitation and analysis tool (OBREAT) [25]. The architecture of OBREAT and the major components can be found in Figure 4.

The presentation layer handles the interaction between users and the application. It checks and takes user input, as well as feedbacks on execution information including reasoning results. Currently, there are a variety of modeling notations, such as UML [26-31], Message Sequence Charts (MSCs) [32], and BPMN [33,34], to visually model the choreography interaction. In our research, the UML class diagrams and collaboration diagrams (or Communication Diagrams in [35]) are preferred for the presentation of service choreography models from structural and behavioral viewpoint, respectively, taking the advantages of rigorous syntax and semantics, easiness to interpret, and various tools such as RSA, EA, and Rose to share some part of models.

As the core component of the architecture, the logic layer processes modeling transactions and submits results to the presentation layer, and it also communicates with the data layer for data persistency. The DL-based Formal Model Generator handles the model conversion with the algorithms mentioned before. The output of the generator is sent to the Model Feature Reasoner and then is saved in Formal Model database. The Model Feature Reasoner communicates with DL reasoner Pellet to complete DL-based reasoning and sends the results to the Execution Control Interface. At present, the Model Feature Reasoner realizes checking the property of consistency, completeness, and state reachability. Specifically, the results are also exported to the Domain Knowledge base to enrich domain knowledge for reuse and thus knowledge reusability is continuously enhanced with knowledge accumulation.

The data layer handles data persistency and maintenance. Most of the input/output data are saved as files, either model files or formalized files, while model management data are saved in the database System Administration Database.

ALGORITHM 1: Construct SHOIN(D) Tbox&Abox. Input: the meta model and the application model Output: Tbox, Abox begin (1) Tbox = [}, Abox = [}; (2) for all MetaConcepts C in meta concept model, do (3) Tbox = Tbox [union] {c}; (4) if [C.sub.2] is the superclass of [C.sub.1], then Tbox = Tbox [union] {[c.sub.1] [subset or equal to] [c.sub.2]}; (5) else if C has a data attribute X (data type is t), then Tbox = Tbox [union] {c [subset or equal to] x x t}; (6) else if [C.sub.1] [not equal to] [C.sub.2] and [C.sub.1] [subset or equal to] [C.sub.2] [not member of] Tbox and [C.sub.2] [subset or equal to] [C.sub.1] [not member of] Tbox, then Tbox = Tbox [union] {[c.sub.1] [PI] [c.sub.2] = [empty set]}; (7) end if ; (8) end for; (9) for all MetaRelation R = ([C.sub.1], [C.sub.2]) in meta concept model, the relation r ~ is the inverse relation of r, do Tbox = Tbox [union] {[c.sub.1] [subset or equal to] [for all]r x [c.sub.2], [c.sub.2] [subset or equal to] [for all][r.sup.~] x [c.sub.1]}; (10) end for; (11) for all the multiplicity constraints in range and domain of every relation R = ([C.sub.1], [C.sub.2]) in meta concept model, the relation r ~ is the inverse relation of r, do (12) if multiplicity constraints is "0 ... 1" then Tbox = Tbox [union] {[c.sub.1] [subset or equal to] [less than or equal to] Ir x [c.sub.2]} [union] {[c.sub.2] [subset or equal to] [less than or equal to] 1[r.sup.~] x [c.sub.1]}; (13) else if multiplicity constraints is " 1 ...*" then Tbox = Tbox [union] {[c.sub.1] [subset or equal to] [greater than or equal to] Ir x [c.sub.2]} [union] {[c.sub.2] [subset or equal to] [greater than or equal to] 1[r.sup.~] x [c.sub.1]}; (14) else if multiplicity constraints is "1" then Tbox = Tbox [union] {[c.sub.1] [subset or equal to] [less than or equal to] 1r x [c.sub.2], [c.sub.1] [subset or equal to][less than or equal to]1r x [c.sub.2]} [union] {[c.sub.2] [subset or equal to][less than or equal to] 1[r.sup.~] x [c.sub.1], [c.sub.2] [subset or equal to][greater than or equal to] 1[r.sup.~] x [c.sub.1]}; (15) end if; (16) end for; (17) return Tbox; (18) for all individuals o in application concept model, (19) if AppFunction(o) = c, do Abox = Abox [union] [o} [union] [o : c}; (20) end for; (21) for all individuals [c.sub.1], [c.sub.2] in application concept model, (22) if AppFunction(r) = R, do Abox = Abox [union] {[c.sub.1]} [union] {[c.sub.2]} [union] [{[c.sub.1],[c.sub.2]) : r}; (23) end for; (24) return Abox; end

For the sake of model exchange, we adopt XML as the model data description language. Since the DL-based reasoner accepts data only in OWL which is somewhat different from XML, the conversion between two types of XML documents is needed. To automate the conversion, we choose the eXtensible Stylesheet Language Transformation (XSLT) technology [36,37] which is widely used for XML document conversion. We designed a set of XSLT transformation templates compliant with the Ontology Definition Metamodel (ODM) and the UML profile. Moreover, we integrate MagicDraw [38] in OBREAT as the GUI modeling tool in the presentation layer and Pellet 1.5.0 as the DL-based reasoner in the logic layer for verification reasoning.

ALGORITHM 2: Construct [R.sub.SWRL]. Input: Deductive reasoning rules for service choreography model Output: Deductive reasoning rules based on SWRL, [R.sub.SWRL] Begin Antecedent = {}, Consequent = {}, Clause = {}; for all concepts C and relations R in prerequisite and conclusion, if [C.sub.1], [C.sub.2] has R relation, [c.sub.1], [c.sub.2] are individuals of [C.sub.1], [C.sub.2], then Clause = Clause [union] {R([C.sub.1][c.sub.1], [C.sub.2] [c.sub.2])}; else if C has a attribute P (type is t), then Clause = Clause [union] [P(Cc, t)}; end for; for all clauses cl do if relation between cl is "and" in prerequisite then Antecedent = Antecedent [union] {[cl.sub.1] [conjunction] [cl.sub.2]}; else if relation between cl is "or" in prerequisite then Antecedent = Antecedent [union] {[cl.sub.1] [disjunction] [cl.sub.2]}; else if relation between cl is "and" in conclusion then Consequent = Consequent [union] {[cl.sub.1] [conjunction] [cl.sub.2]}; else if relation between cl is "or" in conclusion then Consequent = Consequent [union] {[cl.sub.1] [disjunction] [cl.sub.2]}; end if; end for; [R.sub.SWRL] = Antecedent [union] Consequent; return [R.sub.SWRL]; end

4. Case Study

In this section, a simplified case of purchase order application of the e-commerce system is studied, illustrating how to construct the application model and how to realize the model verification.

4.1. Construction of Application Model. Limited by the page size, the choreography of the purchase order application is simplified here, and it covers only a few main activities: the buyer sends an order request to the seller, and then the seller checks the buyer's credit record in the bank and the supplier inventory. If the credit record is good and the inventory is sufficient, then the order will be accepted; otherwise, it will be rejected.

The above activities are encapsulated into five sessions: purchase order request (S-poReq), credit check (S.credChe), inventory check (SJnvChe), purchase order response (S-poResp), and purchase order reject (S-poRej), where there are four participant roles: Buyer, Seller, Bank, and Supplier.

The buyer initiates an interaction with the seller by placing a purchase order po through the channel Ch@Seller, and then the seller acknowledges the buyer by sending him a poAck. Meanwhile, the states of the purchase orders of Buyer and Seller are set to "sent" and "received," respectively. Accordingly, the session S.poReq is composed of four atomic sessions which are specified as follows and is modeled as a UML class diagram in Figure 5:

[mathematical expression not reproducible] (18)

The other four sessions function as follows: S_credChe checks the buyer's credit by sending a request to the bank that sends back the state of the credit (good or bad); S_invChe checks the seller's inventory by sending a request to the seller who sends back the state of the inventory (sufficient or short); S_poResp declares that the order has been accepted if the buyer's credit is good and the inventory is sufficient; and S-poRej declares that the order has been rejected if the buyer's credit is bad or the inventory is short. The four sessions are specified as follows, while the related class models are omitted due to space limitation:

[mathematical expression not reproducible] (19)

The interaction sequence companied with the participants and key messages can be modeled as a UML communication diagram, as shown in Figure 6.

Having analyzed the interaction and the functions of the sessions, we can organize the choreography of the purchase order application as follows:

Cho_po = S_poReq x (S_credChe [parallel] S_invChe) x (S_poResp + S_poRej) (20)

and specify the preconditions of the sessions as follows:

[mathematical expression not reproducible]. (21)

Furthermore, the SHOIN(D) ontology can be generated by the algorithm Construct Tbox&Abox, and as a result, the axiom set in Tbox and the instance set in Abox are listed as in Table 3.

4.2. Verification of Application Model. Having constructed the application model which is subsequently converted into the SHOIN(D) ontology, we can check the correctness properties of consistency, completeness, and state reachability of the specified choreography separately in the following cases.

Case 1 (consistency checking). Consistency checking is to check whether there is a conceptual conflict against modeling semantics; that is, giving a group of related concepts in the application model, the relationships defined between the concepts should semantically abide by the metarelation declared in the metamodel.

Suppose that the modeler tries to add in the application model a relation of Executing between the Role Buyer and the session S_poReq. But according to the constraints of the metamodel, such relation should only appear between two sessions and thus the consistency rule [R.sub.con1] is broken. The error can be easily found through ontology consistency checking using Pellet.

Case 2 (completeness checking). The completeness checking is to check whether there is a lack of concept or relation in the application model; that is, giving a group of related concepts, the relationships defined between the concepts should quantitatively abide by the multiplicity constraint of the corresponding metarelation in the metamodel.

Suppose that the modeler tries to build a Belong_to relation between the Role Supplier and the Participant ProductTrader, meaning that Supplier belongs to a product trader, but wrongly add at the same time another Belong_to relation between Supplier and ServiceProvider. Such relation violates the multiplicity constraint [R.sub.con1] that means each Role must belong to only one Participant at any time. The checking result is prompted by Pellet as follows: "Consistent: No Reason: The individual Supplier has more than one value for property Belong_to violating the cardinality restriction."

Case 3 (state reachability checking). The state reachability checking is to examine whether the termination state of a session defined in the application model is reachable; that is, the session can be deduced using the deductive reasoning rules given in Section 2.1.3. If all sessions are deducible, implying that all session states are reachable, the application behavior is verified.

Session S_poReq is deduced with the deductive reasoning rules [R.sub.atom] and [R.sub.seq2] and as a result poState of Buyer will be set to "sent" and the poState of Seller will be set to "received." The reasoning process is shown as follows:

[mathematical expression not reproducible] (22)

The other four sessions credit check (S_credChe), inventory check (S_invChe), purchase order response (S-poResp), and purchase order reject (S.poRej) can be deduced in the same way.

The whole reasoning process for the application choreography model Cho-po is shown as follows, where the deduction rules applied to each step are bracketed with <>:

[mathematical expression not reproducible] (23)

The atomic sessions in each step are as follows:

[mathematical expression not reproducible] (24)

The application behavior is proven correct provided that the reasoning process may eventually end by NULL. Otherwise, there must be a session failed to be deduced (i.e., its termination state is not reachable). If the application may reach the final state, the key attribute poState of both Buyer and Seller will be set to either "completed" or "uncompleted" (this may happen when Byuer.ccResp = "bad' or Seller.icResp = "short").

To give a negative example, we deliberately assign Seller.poState = "" to make false the precondition P_credChe. As a result, the reasoning process rests on the second step, as the session S_credChe cannot be deduced, and therefore all states of the sessions followed cannot be reached. The exception can be found by entering the following DL-based query command in the form of SPARQL [24]:

SELECT ? a WHERE {? a rdf:type xmlns: Session.? a xmlns: SessionDeduction ? NULL.}.

Figure 7 shows the query result in the human interface panel of the reasoner Pellet, indicating that the session S_poReq and its four atomic sessions are deduced (or can be successfully executed), while all of the subsequent sessions are not shown (or the corresponding states of these sessions may not be reached). The rules <[R.sub.atom], [R.sub.seq2]> are applied to the reasoning process to find the exception where the SessionDeduction relation is broken between the sessions S_poReq and S_credChe and all of the followed sessions cannot be deduced.

Beside the above experiment, we have also modeled and verified several other cases, including the online shopping example given in [39], the buyer-seller example given in [40], and the example from the supply chain management [41].

The verification is processed efficiently. The reasoning for each case is finished within a second, tested on a laptop computer with a 2 GHz Intel processor and 1 GB of RAM. That accords with the comments by Haarslev and Moller [42] who pointed out that even for the hardest problems the query time for DL reasoning would be within three seconds. But, is it always true?

In order to evaluate the efficiency of reasoning for CML-DL models, we choose the four popular ontologies, VICODI, LUBM, Semintec, and Wine which are used in previous benchmarks, carry out experiment, and lead a statistical analysis by comparing the average response times against the increasing size of Abox. The detailed descriptions about these ontologies can be found in [43].

The ontologies represent four standard benchmark datasets with different complexity. The VICODI ontology is relatively small and simple since it does not contain any disjunctions, existential quantification, or number restrictions. The LUBM ontology and the Semintec ontology are also relatively simple like the VICODI ontology, while the Semintec ontology is more complex since it contains functional properties and disjointness constraints and is constructed using OWL DL. The Wine ontology is the most complex one. It contains a classification of wines and is established using advanced DL constructors.

The above ontologies are too small in Abox for our intended performance evaluations. Therefore, we generate different sizes of datasets, ranging from 100 to 1 million, to increase the Aboxes of the ontologies for test.

To evaluate the query times for various sizes of the datasets, we use several query patterns covering all cases from the simplest one that retrieves all individuals of one concept to the most complex one that retrieves all individuals of the concept. The test method can be referenced by [44].

Figure 8 shows the average time for query response for the four ontologies with the generated datasets sizing from 100 to 1 Mio. All the results reported are averaged over 100 queries. The test is led on a laptop computer with one 2 GHz Intel processor and 1GB of RAM, running Windows XP Service Pack 4.

As expected, there is a significant increase of query time as the size of the ontology increases from the 100 to 1 million. For the example of the Semintec ontology, the average query time for smaller size from 100 to 10,000 is less than a second (<1). But, the time increases sharply as the size exceeds 10,000, and for the maximum size of 1 Mio., the time is about 800 seconds or about 17 minutes.

Our ontology of CML-DL may match the Semintec ontology since the domain of the CML-DL application is not more complex than that of the financial services, and the model can be constructed using a fragment of OWL DL without advanced DL constructors. Therefore, we expect that the number of individuals of the CML-DL application model, for most projects, would be less than 100000, and thus the reasoning time would be within a few minutes at worst.

5. Related Work Discussion

System verification accounts for a larger proportion in the domain of system engineering. There are two categories: testing and formal verification. Testing is the process in which testers input the use case through access point and then observe the corresponding output to discover potential error. Formal verification, which can be further divided into model checking based on exhausting searching and model verification based on logic reasoning, expresses system specification by using mathematical methods and then proves whether the designed system meets the desired properties according to mathematical theory.

The initial progress of testing static system properties converts static properties into hard-code and calls these codes during program compilation. Because system specification and system implementation are bounded together, the method does not have flexibility and reusability; that is, when the system static properties to be checked change, the hardcode must be updated as well [45].

The emergence of the open-source projects WS-CDL Eclipse Plugin [46] and Pi4SOA [47] makes it possible to separate system specification and implementation. The engines of these projects provide an execution and simulation environment for WS-CDL documents. When the properties to be checked change, the corresponding descriptions can be revised without any modification to the inspection program. Reference [48] notes that although the WS-CDL is just a description language, it is essentially an XML document; therefore, Eclipse Plugin simulators regard the WS-CDL as executable script language for interpretation and implementation. Nevertheless, the verification methods based on the simulation engine need to traverse the entire value space when handling existential and universal quantifiers, leading to a higher complexity of time and space.

Workflow based web service composition and formal verification techniques are broadly applied. They can be divided into three categories: PN- (Petri Net-) based, FSA-(Finite State Automate-) based, and PA- (process algebra-) based techniques.

Xia et al. [49,50] achieved the complete conversion from a WS-CDL document to stochastic Petri Nets; moreover, they make assessments of time expectations, probability, and cost expectations of services that normally end due to the index of performance, reliability, and execution cost, respectively. Foster et al. [51] proposed a type of service modeling and verification method called model-based service compositions engineering for the first time. The method maps the service composition model to a finite state process (FSP), aiming at verifying the compatibility between composite services and their environment by using a labeled transition system analyzer (LTSA). Molina-Jimenez and Shrivastava [52] developed the concept of conformance between a contract and a choreography by assuming that they can be modeled by Finite Automaton (FA). The choreography specifications and contracts, specified by the BPMN notation and the event-condition-action rules, describe permissible interactions between partners from different viewpoints. They established a process to automatically check whether all the behaviors permissible in a choreography are also permissible in the corresponding contract and vice versa. Diaz and Llana [53] mapped the service composition model in WS-CDL to a timed automation and then simulated the dynamic behavior of the system using the automatic verification tool UPPAAL. The literature [54] provided the basis for formalizing and reasoning on the mobility characteristics of web services choreography using the process algebra [pi]-calculus which is, according to Robin Milner, a model of concurrent computation based on the notion of naming. They argued that the process algebras, such as [pi]-calculus, can be used to formalize web services characteristics to ensure that they satisfy some conditions required in SOA. Salaun et al. [55] presented a method of encoding the collaboration diagrams into the LOTOS process algebra. This encoding allows checking realizability of the collaboration diagrams for both synchronous communication and bounded asynchronous communication.

Gu et al. [8,9] presented a formal modeling framework Abstract WS-CDL with grammar, congruence relations, and operational semantics. They defined a set of mappings of the Abstract WS-CDL global model to the Pi calculus-based local model and accordingly suggested a set of deductive reasoning rules of state reachability and terminability. Unfortunately, they failed to provide the consistency and completeness verification mechanism as well as the corresponding reasoning engine.

Temporal logic (TL) can be used to assert the behavior change with time evolution. The model verification techniques based on TL model the finite states of systems with Promela and specify the system properties with TL expressions to enable verification by checking whether the intersection between the Promela models and the TL expressions is empty. Zhang and Liu [56] presented a formal verification method for CCML (Cooperative Composition Modeling Language) based web service composition. They build a mapping of CCML description to CCS expression and approach property verification and service compatibility verification with the help of a TL based checking mechanism and an automated tool.

The above verification methods, either based on workflow or based on TL, may lead an exhaustive search for all states of system execution, which may cause the state explosion problem when the number of the states exponentially increases as the system scales up.

The DL-based logic reasoning technique is applied to service modeling and verification. Liu et al. [57] proposed a service modeling and composition method based on DL rules using a uniform way of characterizing the static semantic and dynamic interaction characteristics of web services. The method unifies the service composition model within the framework of DL rules to remedy the defect that DL cannot describe the dynamic characteristics of web services. Chang et al. [58,59] proposed an Extended Dynamic Description Logic EDDL(X) by extending the traditional Dynamic Description Logic (DDL) to transform the web service composition model into the EDDL(X)-based one. However, the above methods focus more on service discovery, service matching, and service composition while addressing less the property verification of service choreography model.

Over the past decade, many organizations and individuals have conducted in-depth and fruitful research in the field of service choreography model verification. Their achievements can be categorized, according to their underlying methods, into hard-coding, simulation engine, workflow, temporal logic, and Abstract WS-CDL. As shown in Table 4, we have made a primary comparison of our method with those techniques by the important features such as description ability, degree of automation, knowledge reusability, efficiency of verification, and state explosion.

Regarding description ability, the methods of hardcoding and the simulation engine rank highest since they allow compiling the XML scripts of WS-CDL models. CMV-DL ranks second high due to the strong ability of induction and high level of abstraction with DL [60]. The methods based on workflow and TL are weak in description ability, because they cannot ensure the completeness of mapping one form of model to another, especially when the model is complex in its structure. The current methods based on PA, for example, provide only a few of simple mapping rules and thus do not guarantee a strict conversion, which may cause loss of semantics during conversion [61].

Automation is an important feature for model verification. Each of the methods listed has related supporting tools, except for Abstract WS-CDL. CMV-DL is graded comparatively high in automation, because it takes advantage of available reasoning engines such as Pellet which are based on the mature algorithm Tableau and which have been integrated into the requirement analysis tool OBREAT.

Regarding knowledge reusability, the workflow based, the TL based, and the other three techniques do not provide the mechanism for knowledge accumulation and reuse, while OBREAT allows enriching domain knowledge by adding new reasoning rules to the Domain Knowledge base and importing the reasoning results back into the knowledge base for further reasoning. But the process relies on human interference and thus the capability is graded low.

The verification efficiency is determined by both human interference and time consumption in validation process. The hard-code method and CMV-DL depend heavily on human interference and therefore are graded lowest. The simulation engine technique needs to traverse the entire value space when handling existential and universal quantifiers, which leads to a higher complexity and therefore a low efficiency. The other three methods, supported by automated tools, work highly efficiently for verification.

When a system has many concurrent components, the state space of system execution might expand infinitely beyond ordinary computation capability. Based on exhaustive search, workflow and TL may suffer from the problem of state explosion which has long been the bottleneck for their development [62]. In contrast, CMV-DL works on deduction reasoning where the space of deduction reasoning is limited by the size of the generated ontology and the computation complexity is decreased by the high efficient reasoner algorithm Tableau [63,64].

In general, CMV-DL has an obvious advantage in knowledge reusability and is free of state explosion without the loss of description ability, and it has a modest degree of automation and efficiency compared to the other methods.

6. Conclusion and Future Work

This paper focuses on service choreography modeling and verification. It proposes a new approach of choreography model verification based on Description Logic to verify the service choreography model based on SHOIN(D) of DL. The main contributions are as follows:

(1) A metaconcept model of service choreography based on WS-CDL is proposed, providing a framework to formally define a service choreography model.

(2) Domain rules of consistency, completeness, and deductive reasoning are defined, enabling formal verification of the service choreography model.

(3) The model transformation algorithms are provided and thus the service choreography model and domain rules can be converted into the DL ontology and model verification can be thereby made automatically with an available reasoner, such as Pellet.

(4) The related work on service choreography verification is investigated. The representative methods are analytically compared with CMV-DL on such features as description ability, degree of automation, knowledge reusability, efficiency of verification, and state explosion.

Currently, CMV-DL focuses only on a few key issues of web service choreography. The goal of the metaconcept model and CMV-DL is to verify several key properties of service choreography models. Therefore, CMV-DL captures only a core set of WS-CDL features while omitting some advanced features, such as exception and finalizing blocks. Future work involves extending the service choreography metaconcept model to cover more properties of WS-CDL, such as the consistency between choreography models and orchestration models. Moreover, the domain rules need to be enriched and improved as the approach is applied to more projects.

http://dx.doi.org/10.1155/2016/8947157

Conflict of Interests

The authors declare that there is no conflict of interests regarding the publication of this paper.

Acknowledgment

The paper work was supported by National Natural Science Foundation of China under Program no. 61273210.

References

[1] R. Khadka, B. Sapkota, L. Ferreira Pires, M. Van Sinderen, and S. Jansen, "Model-driven approach to enterprise interoperability at the technical service level," Computers in Industry, vol. 64, no. 8, pp. 951-965, 2013.

[2] Q. Z. Sheng, X. Qiao, A. V. Vasilakos, C. Szabo, S. Bourne, and X. Xu, "Web services composition: a decade's overview," Information Sciences, vol. 280, pp. 218-238, 2014.

[3] N. Kavantzas, D. Burdett, G. Ritzinger et al., Web Services Choreography Description Language Version 1.0, W3C Candidate Recommendation, 2005.

[4] F.-X. Xiao, Z.-Q. Huang, Z.-N. Cao, L.-Z. Tu, and Y. Zhu, "Unified formal modeling and analyzing both functionality and qos of web services composition," Journal of Software, vol. 22, no. 11, pp. 2698-2715, 2011.

[5] M. E. Cambronero, G. Diaz, V. Valero, and E. Martinez, "Validation and verification of web services choreographies by using timed automata," Journal of Logic and Algebraic Programming, vol. 80, no. 1, pp. 25-49, 2011.

[6] L. Zhou, J. Ping, H. Xiao, Z. Wang, G. Pu, and Z. Ding, "Automatically testing web services choreography with assertions," in Formal Methods and Software Engineering, vol. 6447 of Lecture Notes in Computer Science, pp. 138-154, Springer, Berlin, Germany, 2010.

[7] F. M. Besson, P. M. B. Leal, F. Kon et al., "Towards automated testing of web service choreographies," in Proceedings of the 6th International Workshop on Automation of Software Testing, pp. 109-110, 2011.

[8] X. Gu and Z. Lu, "A formal model for BPEL4WS description of Web service composition," Wuhan University Journal of Natural Sciences, vol. 11, no. 5, pp. 1311-1319, 2006.

[9] X. Gu, R. Li, and Z. Lu, "Typed formal model for WS-CDL specification of web services composition," Journal of Southeast University, vol. 24, no. 3, pp. 300-307, 2008.

[10] S. Halle and T. Bultan, "Realizability analysis for message-based interactions using shared-state projections," in Proceedings of the 18th ACM SIGSOFT International Symposium on the Foundations of Software Engineering, pp. 27-36, November 2010.

[11] A. McNeile, "Protocol contracts with application to choreographed multiparty collaborations," Service Oriented Computing & Applications, vol. 4, no. 2, pp. 109-136, 2010.

[12] S. Basu, T. Bultan, and M. Ouederni, "Deciding choreography realizability," Acm Sigplan Notices, vol. 47, no. 1, pp. 191-201, 2012.

[13] W. L. Yeung, "A formal and visual modeling approach to choreography based web services composition and conformance verification," Expert Systems with Applications, vol. 38, no. 10, pp. 12772-12785, 2011.

[14] R. J. Brachman and J. G. Schmolze, "An overview of the KL-ONE knowledge representation system," Cognitive Science, vol. 9, no. 2, pp. 171-216, 1985.

[15] P. Cimiano, C. Uuger, and J. McCrae, Ontology-Based Interpretation of Natural Language, Morgan & Claypool Publishers, 2014.

[16] Web Ontology Language (OWL), World Wide Web Consortium (W3C), 2014, http://www.w3.org/2004/OWL.

[17] J. A. Khan and S. Kumar, "OWL, RDF, RDFS inference derivation using Jena semantic framework & pellet reasoner," in Proceedings of the International Conference on Advances in Engineering and Technology Research (ICAETR '14), pp. 1-8, IEEE, Unnao, India, August 2014.

[18] D. Rodriguez, E. Garcia, S. Sanchez, and C. R.-S. Nuzzi, "Defining software process model constraints with rules using OWL and SWRL," International Journal of Software Engineering and Knowledge Engineering, vol. 20, no. 4, pp. 533-548, 2010.

[19] Object Management Group (OMG), Meta Object Facility (MOF) Core Specification Version 2.0, 2006, http://www.omg .org/spec/MOF/2.0/PDF.

[20] Q. Dong, Z. Wang, W. Zhu, andH. He, "Capability requirements modeling and verification based on fuzzy ontology," Journal of Systems Engineering and Electronics, vol. 23, no. 1, pp. 78-87, 2012.

[21] A. Queralt, G. Rull, E. Teniente, C. Farre, and T. Urpi, "AuRUS: automated reasoning on UML/OCL schemas," in Conceptual Modeling--ER 2010, vol. 6412 of Lecture Notes in Computer Science, pp. 438-444, Springer, Berlin, Germany, 2010.

[22] Q.-C. Dong, Z.-X. Wang, G.-Y. Chen, J. Xin, and T.-T. Zhang, "Domain-specific modeling and verification for C4ISR capability requirements," Journal of Central South University of Technology, vol. 19, no. 5, pp. 1334-1340, 2012.

[23] Q. Dong, Research on formal analysis framework of effectiveness concept of C4ISR systems [Ph.D. thesis], PLA University of Science and Technology, 2013.

[24] H. He, Z. Wang, Q. Dong, W. Zhang, and W. Zhu, "Ontology-based semantic verification for UML behavioral models," International Journal of Software Engineering and Knowledge Engineering, vol. 23, no. 2, pp. 117-145, 2013.

[25] Y. Zhang, Research on key techniques for service-oriented C4ISR capability requirements analysis, modeling and design [Ph.D. thesis], PLA University of Science and Technology, 2012.

[26] T. Bultan and X. Fu, "Specification of realizable service conversations using collaboration diagrams," Service Oriented Computing & Applications, vol. 2, no. 1, pp. 27-39, 2008.

[27] J. Su, T. Bultan, X. Fu, and X. Zhao, "Towards a theory of web service choreographies," in Web Services and Formal Methods: 4th International Workshop, WS-FM 2007, Brisbane, Australia, September 28-29, 2007. Proceedings, vol. 4937 of Lecture Notes in Computer Science, pp. 1-16, Springer, Berlin, Germany, 2008.

[28] T. Bultan and X. Fu, "Choreography modeling and analysis with collaboration diagrams," Bulletin of the Technical Committee on Data Engineering, no. 3, 2008.

[29] I. Yahmadi, Y. Baghdadi, and Z. Al-Khanjari, "Graphical description of WS-CDL," in Proceedings of the 9th International Conference on Innovations in Information Technology (IIT '13), vol. 4, pp. 192-197, March 2013.

[30] M. Emilia Cambronero, V. Valero, and E. Martinez, "Design and generation of Web services choreographies with time constraints," Journal of Universal Computer Science, vol. 17, no. 13, pp. 1800-1829, 2011.

[31] A. Mellat, N. Nematbakhsh, A. Farahi, and F. Mardukhi, "Suitability of uml state machine for modeling choreography of services," International Journal of Web & Semantic Technology, vol. 2, no. 4, pp. 33-53, 2011.

[32] H. Foster, S. Uchitel, J. Magee, and J. Kramer, "An integrated workbench for model-based engineering of service compositions," IEEE Transactions on Services Computing, vol. 3, no. 2, pp. 131-144, 2010.

[33] M. V. Rosing, S. White, F. Cummins et al., "Business process model and notation--BPMN," in Business Process Management Handbook, pp. 429-453, 2015.

[34] M. Cortes-Cornax, S. Dupuy-Chessa, D. Rieu, and N. Mandran, "Evaluating the appropriateness of the BPMN 2.0 standard for modeling service choreographies: using an extended quality framework," Software & Systems Modeling, 2014.

[35] OMG, OMG Unified Modeling Language (OMG UML), Superstructure, V.2.1.2, 2007, http://www.omg.org/spec/UML/2.1.2/ Infrastructure/PDF.

[36] D. Li, X. Li, and V. Stolz, "QVT-based model transformation using XSLT," Acm Sigsoft Software Engineering Notes, vol. 36, no. 1, pp. 1-8, 2011.

[37] A. Belghiat and M. Bourahla, "Transformation of UML models towards OWL ontologies," in Proceedings of the 6th International Conference on Sciences of Electronics, Technologies of Information and Telecommunications (SETIT '12), pp. 840-846, March 2012.

[38] No Magic, MagicDraw Technical Overview, 2015, http://www .nomagic.com/products/magicdraw.html.

[39] J. Su and Y. Sun, "Choreography revisited," in Web Services and Formal Methods, vol. 8379 of Lecture Notes in Computer Science, pp. 13-25, Springer, 2014.

[40] S. Wieczorek, Modeling and Model-Based Testing of Service Choreographies, Akademische Verlagsgemeinschaft Munchen, 2011.

[41] A. Barros, T. Hettel, and C. Flender, "Process choreography modeling," in Handbook on Business Process Management 1, International Handbooks on Information Systems, pp. 257-277, Springer, Berlin, Germany, 2010.

[42] V. Haarslev and R. Moller, "Consistency testing: the race experience," in Automated Reasoning with Analytic Tableaux and Related Methods, vol. 1847 of Lecture Notes in Computer Science, pp. 57-61, Springer, Berlin, Germany, 2000.

[43] B. Motik and U. Sattler, "A comparison of reasoning techniques for querying large description logic Aboxes," in Logic for Programming, Artificial Intelligence, and Reasoning: 13th International Conference, LPAR 2006, Phnom Penh, Cambodia, November 13-17, 2006. Proceedings, vol. 4246 of Lecture Notes in Computer Science, pp. 227-241, Springer, Berlin, Germany, 2006.

[44] P. Cimiano, P. Haase, Q. Ji et al., "Reasoning with large a-boxes in fuzzy description logics using dl reasoners: an experimental evaluation," in Proceedings of the ESWC Workshop on Advancing Reasoning on the Web Scalability & Commonsense, 2008.

[45] Z. Wang, L. Zhou, Y. Zhao et al., "Web services choreography validation," Service Oriented Computing and Applications, vol. 4, no. 4, pp. 291-305, 2010.

[46] WS-CDL Eclipse Plugin, 2014, http://wscdl-eclipse.sourceforge .net.

[47] C. Das and P. Bhuyan, "A systematic survey report on various frameworks and models for verification of choreography in SOA," Journal of Computer Science & Engineering Technology, vol. 5, no. 4, pp. 411-418, 2014.

[48] F. Besson, A framework for automated testing of web service choreographies [Ph.D. thesis], University of Sao Paulo, Sao Paulo, Brazil, 2011.

[49] Y. Xia, H. Xue, and X. Wang, "Performance prediction of WS-CDL based service composition," in Proceedings of the 10th International Conference on Quality Software (QSIC '10), pp. 294-299, July 2010.

[50] Y. Dong, Y. Xia, T. Sun, and Q. Zhu, "Modeling and performance evaluation of service choreography based on stochastic Petri net," Journal of Computers, vol. 5, no. 4, pp. 516-523, 2010.

[51] H. Foster, S. Uchitel, J. Magee, and J. Kramer, "An integrated workbench for model-based engineering of service compositions," IEEE Transactions on Services Computing, vol. 3, no. 2, pp. 131-144, 2010.

[52] C. Molina-Jimenez and S. Shrivastava, "Establishing conformance between contracts and choreographies," in Proceedings of the 15th IEEE Conference on Business Informatics (CBI '13), pp. 69-78, IEEE, Vienna, Austria, July 2013.

[53] G. Diaz and L. Llana, "Contract compliance monitoring of web services," in Service-Oriented and Cloud Computing, vol. 8135 of Lecture Notes in Computer Science, pp. 119-133, Springer, Berlin, Germany, 2013.

[54] P. Nduwimfura, D. Xu, H. Miao, Z. Lei, and B. Chen, "Reasoning on formalizing WS-CDL mobility using process algebra," in Proceedings of the IEEE Asia-Pacific Services Computing Conference (APSCC '10), pp. 676-682, December 2010.

[55] G. Salaun, T. Bultan, and N. Roohi, "Realizability of choreographies using process algebra encodings," IEEE Transactions on Services Computing, vol. 5, no. 3, pp. 290-304, 2012.

[56] X. Zhang and H. Liu, "Formal verification for CCML based web service composition," Information Technology Journal, vol. 10, no. 9, pp. 1692-1700, 2011.

[57] S. Liu, D. Liu, H. Qi, and J. Guan, "Composing semantic web service with description logic rules," Journal of Computer Research and Development, vol. 48, no. 5, pp. 831-840, 2011.

[58] L. Chang, Z. Z. Shi, L. M. Chen, and W. Niu, "Family of extended dynamic description logics," Journal of Software, vol. 21, no. 1, pp. 1-13, 2010.

[59] L. Chang, Z. Shi, T. Gu, and L. Zhao, "A family of dynamic description logics for representing and reasoning about actions," Journal of Automated Reasoning, vol. 49, no. 1, pp. 1-52, 2012.

[60] B. B. Hariri, D. Calvanese, M. Montali, G. de Giacomo, R. De Masellis, and P. Felli, "Description logic knowledge and action bases," Journal of Artificial Intelligence Research, vol. 46, pp. 651-686, 2013.

[61] Z. Huang, F. Xiao, and L. Tu, "Modeling service composition using priced probabilistic process algebra," in Proceedings of the 5th IEEE International Symposium on Service-Oriented System Engineering (SOSE '10), pp. 35-38, June 2010.

[62] P. Drobintsev, V. P. Kotlyarov, and I. V. Nikiforov, "Technology aspects of state explosion problem resolving for industrial software design," in Proceedings of the Spring/Summer Young Researchers' Colloquium on Software Engineering, pp. 46-51, Kazan, Russia, May 2013.

[63] S. Ben-David, R. Trefler, and G. Weddell, "Model checking using description logic," Journal of Logic & Computation, vol. 20, no. 1, pp. 111-131, 2010.

[64] E. M. Clarke, W. Klieber, M. Novacek, and P. Zuliani, "Model checking and the state explosion problem," in Tools for Practical Software Verification, vol. 7682 of Lecture Notes in Computer Science, pp. 1-30, Springer, Berlin, Germany, 2012.

Institute of Command Information System, PLA University of Science and Technology, Nanjing 210007, China

Correspondence should be addressed to Zhixue Wang; wzxcx@163.com

Received 9 May 2015; Revised 23 June 2015; Accepted 14 July 2015

Academic Editor: Jean-Francois Monin

Caption: Figure 1: Service choreography modeling framework.

Caption: Figure 2: Metamodel of service choreography based on WS-CDL.

Caption: Figure 3: Mechanism for service choreography model verification based on SHOIN(D).

Caption: Figure 4: Architecture of service hierarchy of OBREAT.

Caption: Figure 5: Structure of S_poReq.

Caption: Figure 6: Interaction between roles in the choreography.

Caption: Figure 7: The query command window for checking the state reachability.

Table 1: A summary of metaconcepts of service choreography for the metamodel (a fragment). Concepts Definition Description Participant Par = <N,Ro> The business entities or web services that participate in service interaction. N is the name and Ro denotes the roles it implements. Role Ro = <N, Op, Ch, Va> The observable behavior a participant exhibits in order to collaborate. Ro initiates the collaborative operations (Op) through channels (Ch) with other roles, and the local variables (Va) will be affected. Activity Act = <N, Ca> The actual functions performed in the choreography. They (Ca) can be categorized into basic activities and structural activities. Precondition P = <N, Boolean> The preconditions of session execution, specified in Boolean type. Guard G = <P, S> The bindings of preconditions to sessions. Variable Va = <N, Ro> The variables a role has. It is a component of a role specification. Operation Op = <N, Ro> The operations a role provides. It is a component of a role specification. Channel Ch = <N, Ro, Loc, Int> The locations and manners through which information is exchanged between roles. Loc and Int denote the channel locations and interaction activities, respectively. Interface In = <N, Par> The declaration of the participants (Par) that collaborate. Port Po = <N, In> The way through which roles interact. One interface may correspond to one role and multiports. Table 2: A summary of metarelations of service choreography for the metamodel (a fragment). Relations Correlative concepts SessionDeduction Session x Session Congruence Session x Session Implement Participant x Role Contain Choreography x Session Link Channel x Role Belong.to Role x Participant HasName Role x Name Provide Role x operation Executing Session x [S.sub.atom] Sequence Session x Session Parallel Session x Session Choice Session x Session WorkUnit Session x Session Relations Formal semantics SessionDeduction Session [subset or equal to] [for all] SessionDeduction. Session Congruence Session [subset or equal to] [for all] Congruence Session Implement Participant [subset or equal to] [for all] Implement.Role Contain Choreography [subset or equal to] [for all] Contain.Session Link Channel [subset or equal to] [for all] Link.Role Belong.to Role [subset or equal to] [for all] Belong.to.Participant HasName Role [subset or equal to] [for all] HasName.Name Provide Role [subset or equal to] [for all] Provide.operation Executing Session [subset or equal to] [for all] Executing. [S.sub.atom] Sequence Session [subset or equal to] [for all] Sequence. Session Parallel Session [subset or equal to] [for all] Parallel. Session Choice Session [subset or equal to] [for all] Choice. Session WorkUnit Session [subset or equal to] [for all] WorkUnit. Session Table 3: Axiom set and instances set of purchase order service choreography model (fragment). Axiom set in Tbox Instances set in Abox S_poReq: [S.sub.com] NoAction [subset or equal to] Abas S_poReq_req: [S.sub.atom] SilentAction [subset or equal to] S_poReq_resp: [S.sub.atom] Abas InterAction [subset or equal to] S-poReq-assign-Buyer: [S.sub.atom] Abas Assign [subset or equal to] Abas S_poReq_assign_Seller: [S.sub.atom] Perform [subset or equal to] Abas S_credChe: [S.sub.com] Abas [subset or equal to] Act S_poResp: [S.sub.com] Astr [subset or equal to] Act ProductTrader: Participant [S.sub.atom] [subset or equal to] ServiceProvider: Participant Session [S.sub.com] [subset or equal to] S.credChe [parallel] S_invChe Session S_Che: [S.sub.parallel] Session [subset or equal to] [for S-poResp + S.poRej: [S.sub.choice] all] SessionDeduction.Session Participant [subset or equal to] Cho_po: Choreography [for all] Implement.Role Choreography [subset or equal to] Buyer: Role [for all] Contain.Session Interaction [subset or equal to] Supplier: Role [for all] Depend.Channel Role [subset or equal to] [for P_credChe: Precondition all] Belong_to.Participant Interface [subset or equal to] <Cho.po, S_poReq>: Contain [for all] Bind.Role Session [subset or equal to] [for <S_credChe, P_credChe>: Guard all] Executing. [S.sub.atom] Session [subset or equal to] <S_poReq, S_poReq_req>: Executing [for all] Sequence. Session Session [subset or equal to] <S_credChe, S_invChe> : Parallel [for all] Choice. Session ... <S_poReq, S_credChe [parallel] S_invChe S_Che>: Sequence Table 4: Comparison between several typical verification methods of service choreography model. Methods Simulation Features Hard-coding engine Workflow Description ability +++ +++ + Degree of automation + + ++ Knowledge reusability - - - Efficiency of verification + ++ +++ State explosion - - + Methods Temporal Abstract Features logic WS-CDL CMV-DL Description ability + + ++ Degree of automation ++ - ++ Knowledge reusability - - + Efficiency of verification +++ + +++ State explosion + - - +: support/existence, -: nonsupport/nonexistent. Figure 8: Average query time for the four ontologies (VICODI, LUBM, Semintec, and Wine). VICODI LUBM Semintec Wine 100 0.064 0.058 0.286 0.833 1000 0.081 0.063 0.37 0.942 10000 0.088 0.086 0.771 68.555 100000 0.831 2.075 100.491 998.45 1000000 79.451 100.011 800.211 1000.981

Printer friendly Cite/link Email Feedback | |

Title Annotation: | Research Article |
---|---|

Author: | Yu, Minggang; Wang, Zhixue; Niu, Xiaoxing |

Publication: | Mathematical Problems in Engineering |

Date: | Jan 1, 2016 |

Words: | 11779 |

Previous Article: | Approximation of Linear Elastic Shells by Curved Triangular Finite Elements Based on Elastic Thick Shells Theory. |

Next Article: | A Self-Adjusting Method to Resist Bus Bunching Based on Boarding Limits. |

Topics: |