Business process modelling and execution in a collaborative environment requires a set of methodologies and tools which support the transition from an analysis to an execution level. Integrating the process with a pre-existing IT infrastructure leads to typical interoperability problems. Service-oriented architectures are today's favorite answer to solve these interoperability issues. To tackle them, the recent trend is to use the principles of model driven-design. In this paper, we apply these principles to Semantic Web service technology to assist a business orchestrator nding suitable services at design time, and composing work ows for agent-based execution. We describe a formal approach to preserve the content of the semantic annotations in the model and code transformations.
Service-oriented architectures (SOA) are today's favorite answer to realize the
vision of seamless business interaction across organizational boundaries. It enables
enterprises to o er selected functionalities of their business systems via
standardized XML-based Web service interfaces (written in WSDL [
The remainder of this paper is structured as follows. We outline the MDSM matchmaking process in section 2. In section 3 we describe the transformation of the service request from the platform-independent to the platform-speci c level. Section 4 gives an example of the whole matchmaking process of MDSM, while section 5 concludes the paper. 2
The MDSM matchmaker is capable of automated, model-independent semantic service selection to assist business service orchestrators in nding suitable services to realize parts of collaborative business processes as adequate service orchestrations at design time. Consider, for example, the modelling of a complex travel planning process as depicted in gure 1. At a certain point of choice in the planning process the human user, that is the business orchestrator, needs to select a ight booking Web service to realize the respective booking process in the overall work ow of travel planning. For this purpose, the orchestrator models her Web service request in the common metamodel she is familiar with only, that is the platform-independent metamodel PIM4SWS.
The MDSM, in its rst implementation, automatically transforms this
request to semantically equivalent service requests in OWL-S, WSML and SAWSDL,
and then issues them to relevant platform-speci c matchmakers, that are for the
implementation of MDSM 1.0, the matchmakers OWLS-MX [13], WSML-MX
[12] and SAWSDL-MX. Eventually the MDSM provides the orchestrator with
an aggregated and ranked answer set of relevant semantic services [
In order to correctly compile a given service request in PIM4SWS to di erent
platform-speci c representations such as OWL-S and WSML, we di erentiate
between (a) structural transformation of the semantic service description as a
whole, and (b) the semantic mapping between corresponding components of
the information model of PIM4SWS such as its input, output, preconditions
and e ects that are described in speci c ontology and rule languages like OWL
[19], SWRL and WSML [27]. While structural transformations of PIM4SWS
representations in UML to OWL-S and WSML are de ned in terms of syntactic
mappings between corresponding modelling concepts, we use the standardized
formal speci cation language Z for the latter purpose (cf. Fig. 3).
The metamodel PIM4SWS is designed as a core model to cover the common
parts of the underlying semantic service description languages. It consists of
three parts: InformationModel (IM; ODMNameSpace), BlackBox and GlasBox
(cf. Fig. 4. The information model is the set service related ontologies described
in the standard metamodel ODM [
We acknowledge that the PIM4SWS metamodel is similar to the OWL-S model which can be to a large extent embedded into the WSML model[15] which makes the structural transformations from PIM4SWS to both speci c models or platforms straight-forward. In particular, the OWL-S service pro le is generated from the Functionals and NonFunctionals of the given PIM4SWS service description, the OWL-S process model for atomic processes is given by the Functionals where the "hasResult" construct of the OWL-S service is extracted from the OECondition. For structural transformations from PIM4SWS to WSML, the following holds: (a) the Service class is related to any service component in WSML; (b) the NonFunctionals class is covered by annotations and non-functional properties of the considered service component; and (c) the Functionals class is mapped to the capability of the service. Since in PIM4SWS inputs and outputs describe information between a service provider and the requester, these classes are related to pre- and postcondition concepts in WSML. Furthermore, we map preconditions to assumptions. The WSML service result construct is resolved by an implication in the postcondition and e ect axiom of WSML, where the antecedent is the semantically transformed OECondition expression, and the consequent is the transformed hasE ect expression for an e ect, and the transformed hasOutput for a postcondition in WSML. Each parameter is handled by initializing shared WSML variables. Due to space limitations, we omit further details of the structural transformation from PIM4SWS to WSML and SAWSDL, and rather focus on the semantic mapping between the PIM4SWS information model (in ODM) and di erent ontology languages (platforms) used for semantic annotation. 3.2
Semantic Transformation using Z
To achieve a veri ably correct mapping between the di erent DL-based ontology
languages used for semantic annotation such as OWL-DL and WSML-DL in our
case, we use the formal standard speci cation language Z as a common basis1.
Based on [
Why then using Z? In principle, the information model of the PIM4SWS is not restricted to our initial choice of a description logic (SHIN(D)) but shall cover di erent ontology and rule languages (in di erent notations) with rstorder logic (FOL) semantics. For this purpose, we suggest to use the ISO standard speci cation language Z (semantically equivalent to FOL) as a common language for specifying semantic annotations of service requests in PIM4SWS by the orchestrator. Please note that the semantic equivalence of PIM4SWS service request annotations in SHIN(D) we proposed for our intial version of the PIM4SWS-IM with those in OWL-DL and WSML-DL of the request in OWL-S and WSML compiled by the MDSM matchmaker is trivial: It holds per de nition of the PIM4SWS-IM as intersection of OWL-DL and WSML-DL both assumed as sole ontology languages for semantic annotations of service requests in PIM4SWS, OWL-S and WSML. In general, testing the semantic equivalence of pairs of platform-independent and platform-dependent semantic service request 1 Z is based on Zermelo-Fraenkel set theory and rst-order predicate logic. It is widely used by industry for system behaviour speci cation and veri cation of properties, and has undergone international ISO standardization. Various tools for formatting, type-checking and aiding proofs in Z are available, e.g. see http://vl.zuser.org/. annotations in di erent rst-order logic-based ontology languages in di erent syntactic representation is to convert them into equivalent FOL expressions and use a FOL theorem prover for checking the satis ability of their mutual logic implication. This semantic equivalence can also be shown using Z as common speci cation language as shown in gure 5.
Fig. 5. Semantically equivalent compilation of annotations in PIM4SWS-IM to OWLDL and WSML-DL using Z.
In particular, having a semantic annotation in the PIM4SWS-IM, we provide
its transformation to Z (step a), which corresponds to the SHIN(D) related part
of the speci cation of OWL-DL, respectively SHOIN(D), in Z (steps b and d,
as reported in [17] with proof of correctness and completeness). Likewise, the
speci cation of the PIM4SWS service request annotation in Z corresponds to the
SHIN(D) related part of the speci cation of WSML-DL, respectively SHIQ(D)
in Z (steps c and d), which, in turn, is a FOL subset (step f, [
The universal signature of the (PIM4SWS-)IM is the set of OntologyElements with the interpretation IIM = (IMIndividual ; IIM ) where IMIndividual is the domain of discourse (according to the set-theoretic rst-order semantics of description logics). The function IIM maps an IMClass c to the subset of the domain (classInstances(c)) and an IMProperty p to a tuple (subject(propVals(p)), object(propVals(p))). The semantics of the initial IM, that is SHIN(D), is then equivalently speci ed by the following Z axioms.
[OntologyElement ] An IMIndividual is modelled as a subset of OntologyElement. IMClass is another subset of OntologyElement disjoint from IMIndividual. The function classInstances maps an IMClass to the IMIndividual set of their instances.
classInstances : IMClass ! P IMIndividual
IMClass \ IMIndividual = ? IMProperty and IMPropertyValue are again subsets of OntologyElement and disjoint to each other and to the above subsets. An instance of an IMProperty is an IMPropertyValue. The function propVals maps an IMProperty to its set of instances.
propVals : IMProperty ! P IMPropertyValue IMProperty \ IMClass = ? IMProperty \ IMIndividual = ? IMPropertyValue \ IMClass = ? IMPropertyValue \ IMIndividual = ? IMPropertyValue \ IMProperty = ? subject : IMPropertyValue $ IMIndividual object : IMPropertyValue $ IMIndividual imSubClassOf : IMClass $ IMClass 8 c1; c2 : IMClass imSubClassOf (c1) = c2 , classInstances(c1) classInstances(c2) Every IMPropertyValue has unary relations, subject and object, that returns two IMIndividuals which are related by the property.
To express a class hierarchy in the metamodel generalizations are used. A generalization relates two classes, where the rst class is a subclass of the second. Universal restricted classes are a subset of an IMClass that are universal restricted to a target IMClass by a given IMProperty.
onProperty : UniRestriction $ IMProperty toClass : UniRestriction $ IMClass
For the Z-speci cation of semantic annotations in OWL-DL, we refer to [17]. In the following, variables in platform-speci c speci cations are marked with a prime like x 0; y 0. The interpretation of the Z-speci cation of OWL-DL expressions is de ned as IOWL = (OWLIndividual ; IOWL ) with the domain OWLIndividual and the interpretation function IOWL mapping an OWLClass c0 to a subset (instances(c0)) of the domain and an OWLProperty p0 to a tuple (subVal(p0)). The corresponding Z axioms for OWL-DL restricted to the IM speci cation in Z are as follows.
[Resource]
OWLIndividual \ OWLClass = ? OWLProperty \ OWLClass = ? OWLProperty \ OWLIndividual = ? instances : OWLClass ! P OWLIndividual subVal : OWLProperty ! (Resource $ Resource) subClassOf : OWLClass $ OWLClass 8 c10; c20 : OWLClass subClassOf (c10) = c20 , instances(c10) instances(c20) allValuesFrom : (OWLClass
Specifying SHIQ(D) of WSML-DL for its subset SHIN(D) of the IM in Z is
the same as we showed for OWL-DL above. That allows to compare the
respective elements of WSML-DL and OWL-DL by looking at their representation in
Z (with di erently renamed elements for better distinction between them) as
shown in table 1. The semantically equivalent transformation from WSML-DL
to the corresponding F-Logic fragment is given in [
S OWLIndividual set of instances AC OWLClass set of atomic concepts AR OWLProperty set of atomic properties IS instances / subVal semantic mapping to the domain subConcept subClassOf concept hierarchy forall allValuesFrom universal quanti er
To verify whether a direct model transformation t (D ) = D 0 of a description D in the platform-independent model PIM4SWS-IM to a description D 0 in platform-speci c model or ontology language is semantically correct, one can test whether the semantics of D and D 0 are equivalent in Z. We show this by example for a description D in IM and D 0 in OWL-DL both transformed to Z. In Zermelo-Fraenkel set theory, the axiom of extensionality de nes the equality of two sets: 8 A 8 B [8 x (x 2 A , x 2 B ) ) A = B ]. Thus, descriptions D and D 0 are semantically equal (sem(D ) = sem(D 0)) i their interpretations in the domain are the same (D I = D 0I ). For reasons of comparability, the domains of discourse of considered ontology languages (models) have to be the same: MIndividual = OWLIndividual = . The element equality in Z is de ned as follows: Let x 2 IMIndividual, y 0 2 OWLIndividual/ , then elements x ; y 0 are the same eql (x ; y 0) = true i sem(x ) = sem(y 0). That allows us to compare the semantic equality of di erent language elements in Z as shown in table 2: Equality of facts (a), sets of instances (b), concepts (c), property values (d), sets of property values according to a given property (e), and properties (f). In fact, we can obtain the semantic equivalence between constructors of the description logics underlying the initial PIM4SWS-IM and those of OWL-DL, respectively WSML-DL denoted in Z. Due to space limitation, we provide only a selection of these Z-equality relations in the following.
We use these elementary Z-equality relations recursively to prove (by structural induction) the semantic equality for any given DL axiom or expression. For example, consider the DL concept subsumption axiom c1 v c2 for two concepts c1; c2. The equality of its description imSubClassOf (in PIM4SWS-IM) and subClassOf (in OWL-DL) can be shown by the equality of their transformation in Z. Let c1; c2 2 IMClass, c10; c20 2 OWLClass/AC, c3 2 UniRestriction, p 2 IMProperty, p0 2 OWLProperty with c1 = c10, c2 = c20, onProperty(c3) = p, toClass(c3) = c1 and p = p0, then the following holds: imSubClassOf (c1) = c2 , classInstances(c1) classInstances(c2) (1) (2) (3) , instances(c10)
instances(c20) , subClassOf (c10) = c20 In line (2) we use the equality relation (b) in table 2 to translate the IM specication of imSubClassOf in Z to OWL-DL, which is the same as subClassOf in OWL-DL. Analogously, we provide the (Z-)equality relation for universal quanti ed role cardinality restrictions (8 R:C in DL syntax): c3 , 8 a1; a2 : IMIndividual a1 2 classInstances(c3) , (9 v : IMPropertyValue j v 2 propVals(p) (subject (v ) = a1 ^ object (v ) = a2) ) a2 2 classInstances(c1) Thus, instances of c3 are equal to instances of the allValuesFrom construct, and determined by the following expression: classInstances(c3) , fx : IMIndividual j 8 a2 : IMIndividual 9 v : IMPropertyValue j v 2 propVals(p) (x = subject (v ) ^ a2 = object (v )) ) a2 2 classInstances(c1)g , fx 0 : OWLIndividual j 8 a20 : OWLIndividual
(x 0; a20) 2 subVal (p0) ) a20 2 instances(c10)g , instances(allValuesFrom(c10; p0))
Based on these Z-equality relations, one can prove that the syntactic model transformation function (t (D ) = D 0) of the MDSM matchmaker from PIM4SWSIM to OWL-DL and WSML-DL is semantically correct. 4
In the following, we brie y illustrate the principle of model-driven service matchmaking by the MDSM matchmaker. Suppose that a business service orchestrator intends to integrate a ight-booking Web service into her business process implementation. The service shall book one ticket for a given ight and customer, and con rms the booking. This request is formulated in PIM4SWS by the orchestrator and passed to the MDSM which transforms the received request to speci c description models, that are, in our case, OWL-S, WSML and SAWSDL. The structural transformations to OWL-S and WSML are depicted in gures 6 and 7.
The semantic transformation of the request concerns all ontological concepts used to describe the service pro le parameters (IOPE). We show this by example for the input concept Flight-Passenger (FP) which is described in the PIM4SWS-IM as shown in gure 8. In the following, we use the abbreviations P for Passenger, FP for FlightPassenger, AP for AirPlane, and V for Vehicle.
The MDSM transforms this description (D ) directly into an equally named concept FP' described (D 0) in OWL-DL: subClassOf(restriction travelsBy' allValuesFrom(AirPlane'), Passenger')
The semantic equivalence of this transformation (t (D ) = D 0) can be shown using Z as follows. Concept FP in the PIM4SWS-IM is speci ed in Z by FP : UniRestriction imSubClassOf (FP ) = P
The denoted equality between concepts in this expression is checked by comparing their extensions: The set of instances of the UniRestriction class FP is given by the set of IMIndividual x which has to be a subset of the instances of concept P: classInstances(FP ) = fx : IMIndividual j
According to the Z-element equality de nition above, and the semantic Z-equality
relations (cf. table 2a-f) of the description logic operations above, the set of
instances of FP (in Z) is equal to the OWLClass FP' (in Z):
instances(FP0) = fx 0 : OWLIndividual j 8 a20 : OWLIndividual
(x 0; a20) 2 subVal (travelsBy0) ) a20 2 instances(AP0)g instances(P0)
Assuming that P = P 0; AP = AP 0 and travelsBy = travelsBy0, the semantic
equivalence of FP (in PIM4SWS-IM) and its transformation FP' (in OWL-DL)
holds. The same is valid for FP' in WSML-DL. FP in SHIQ(D) can be speci ed
in Z: forall travelsBy'.AirPlane' v Passenger' This expression can be
equivalently written in FOL, F-Logic [
in F-Logic: 8 x :(8 y:x [travelsBy0 y] y : AirPlane0) x : Passenger 0); in WSML-DL: forall ?y( ?x [travelsBy' hasValue ?y] implies ?y memberOf AirPlane') implies ?x memberOf Passenger' Fig. 8. Part of the PIM4SWS information model for service input concept FlightPassenger (FP).
The compiled service request in OWL-S, WSML and SAWSDL is passed by the MDSM to its integrated platform-speci c matchmakers. Their ranked answer sets are aggregated and eventually presented by the MDSM to the orchestrator. 5
We provided a rst approach to model-driven semantic Web service selection to support business process orchestrators at design time. In its inital version, our model-driven service matchmaker MDSM 1.0 is restricted to (a) speci c matchmakers for OWL-S, WSML and SAWSDL, and (b) a platform-independent information model de ned as intersection of OWL-DL and WSML-DL. However, the principle of model-driven semantic selection applies to other ontology languages and speci c matchmakers to be plugged into the MDSM as well. Future work covers the extension of the PIM4SWS information model with OCL constraints, and transformations to SWRL and WSML-Rule [25, 24]. 7. de Bruijn, J., Heymans, S.: WSML Ontology Semantics. WSML Final Draft, Available: http://www.wsmo.org/TR/d28/d28.3/v0.1/20061218/, 2006. 8. Duke, R., Rose, G.: Formal Object Oriented Speci cation Using Object-Z. Cornerstones of Computing, Macmillan, 2000. 9. Duric, D.: MDA-based Ontology Infrastructure. Intl. Journal on Computer Science and Information Systems, Vol. 1, No. 1, 2004. 10. Gannod, G. C., et al.: Faciliating the Speci cation of Semantic Web Services Using
Model-Driven Development. Journal of Web Services Research, 2006. 11. Gr nmo, et al.: Transformations between UML and OWL-S. European Conf. on Model Driven Architecture - Foundations and Applications (ECMDA-FA), Nurnberg, Germany, 2005. 12. Kaufer, F., Klusch, M.: WSMO-MX: A Logic Programming Based Hybrid Service Matchmaker. Proc. of the IEEE Intl. Conf. on Systems, Man and Cybernetics, Montreal, Canada, 2007. 13. Klusch, M., et al.: OWLS-MX: Hybrid Semantic Web Service Retrieval. Proc. of the 1st Intl. AAAI Fall Symposium on Agents and the Semantic Web, Arlington VA, USA, 2005. 14. Koehler, J., et al.: The role of visual modeling and model transformations in business-driven development. In 5th Intl. Workshop on Graph Transformation and Visual Modeling Techniques, 2006. 15. Lara, R., Polleres, A.: Formal Mapping and Tool to OWL-S. Available: http://www.wsmo.org/2004/d4/d4.2/v0.1/20041217/ 16. Lautenbacher, F., Bauer, B.: Creating a Meta-Model for Semantic Web Service Standards. Proc. of the 3rd Intl. Conf. on Web Information System and Technologies (WEBIST) - Web Interfaces and Applications, Barcelona, Spain, 2007. 17. Lucanu, D., et al.: Web Ontology Veri cation and Analysis in the Z Framework.
TR 05-01, Faculty of Computer Science, University Alexandru Ioan Cuza, 2005. 18. OWL-S: Semantic Markup for Web Services, W3C Member Submission, Available: http://www.w3.org/Submission/2004/SUBM-OWL-S-20041122/, 2004. 19. OWL Web Ontology Language Reference, W3C Recommendation, Available: http://www.w3.org/TR/2004/REC-owl-ref-20040210/, 2004. 20. Rector, A., Schreiber, G.: Quali ed cardinality restrictions (QCRs): Constraining the number of values of a particular type for a property. W3C Editor's Draft, Available: http://www.cs.vu.nl/ guus/public/qcr-20060508.html, 2006. 21. Scicluna, J.; et al. (2004): Formal Mapping and Tool to OWL-S. WSMO Working
Draft 17 December 2004, Available: http://www.wsmo.org/TR/d4/d4.2/v0.1/. 22. Semantic Annotations for WSDL and XML Schema, W3C Recommendation, Available: http://www.w3.org/TR/2007/REC-sawsdl-20070828/, 2007. 23. Spivey, M.: The Z Notation: A Reference Manual, 2nd edition. Prentice Hall International Series in Computer Science, 1992. 24. Wang, H. H., et al.: A Formal Semantic Model of the Semantic Web Service Ontology (WSMO). 12th IEEE Intl. Conf. on Engineering of Complex Computer Systems, Auckland, New Zealand, 2007. 25. Wang, H. H., et al.: Formal Speci cation of OWL-S with Object-Z. The First
ESWC Workshop on OWL-S: Experiences and Future Directions, Austria, 2007. 26. Web Service Modeling Ontology (WSMO), W3C Member Submission, Available: http://www.w3.org/Submission/2005/SUBM-WSMO-20050603/, 2005. 27. Web Service Modeling Language (WSML), W3C Member Submission, Available: http://www.w3.org/Submission/2005/SUBM-WSML-20050603/, 2005.