ICAASE'2014 Specification and Verification of Timed Semantic web Services Specification and Verification of Timed Semantic web Services Amel Boumaza Ramdane Maameri LIRE laboratory, Constantine 2 University LIRE laboratory, Constantine 2 University Constantine, Algeria Constantine, Algeria Spd_ing2006@yahoo.fr ramdane.maamri@univ-constantine2.dz Abstract – It is widely recognized that temporal aspects are indispensable for Web Service modeling. Unfortunately, the current Semantic web Services description languages suffer from the lack of useful concepts needed for timing description. For this purpose, we propose a global methodology for the specification of timing behavior with an extended OWL-S ontology and verification of temporal properties with UPPPAL tool. The applicability is illustrated through the multimodal transport use case. Keywords –Web Services, OWL-s, Entry Sub-Ontology Of Time, Timed Automata, Uppaal Temporal Properties of these are based on state-action models (e.g. labeled transition systems, timed automata, and 1. INTRODUCTION Petri nets) or process models (e.g. π-calculus and other calculi) [1]. Automatic composition is the capability to automatically compose a set of services to fulfill user requirements when a single service is not 2. Related works available for fulfilling these requirements. Composing services need an approach based Recently, a diversity of concrete proposals from on semantic descriptions, as the requester the formal methods community have emerged in required functionally has to be expressed in a order to verify the correctness of the web service high-level and abstract way to enable reasoning composition which is based on state action procedures. models or process models [2]. Efficiently, the semantic web community allows In [3], a case study is presented that shows how reasoning about web resources by explicitly descriptions of web services written in BPEL- declaring their preconditions and effects with WSCDL (Web Services Choregraphy terms defined precisely in ontologies. Description Language) can be automatically Furthermore, in Semantic Web Services, the translated to timed automata and subsequently common need for temporal information is be verified by Uppaal. satisfied by the use of the temporal ontologies to In [4] the authors provide an encoding of BPEL allow using of temporal concepts. However, the processes into web service timed state transition complexity comes usually with the growing systems and discuss a framework in which expressiveness; it becomes a challenging area timed assumptions expressed in the duration to ensure correctness. Hence, the verification of calculus [5] can be model checked. Web Service flow becomes more and more In [6] a framework to automatically verify important. systems that are modeled in Orc1 is proposed. Formal methods are particularly well appropriate to address most of the aforementioned issues 1 Home page: http://orc.csres.utexas.edu/ (e.g. composition and correctness). The majority International Conference on Advanced Aspects of Software Engineering ICAASE, November, 2-4, 2014, Constantine, Algeria. 83 ICAASE'2014 Specification and Verification of Timed Semantic web Services Uppaal can be used to model check Orc models. service by using a semantic model, in which The approach is demonstrated through a small each implicated atomic process is described case study. semantically in terms of inputs, preconditions, In [7], the authors deal with the compatibility outputs, and effects (IPOEs). problem. The proposed framework allows Composite processes are used to describe applying model checker Uppaal to asynchronous collections of processes (either atomic or Web services composition analysis by using a composite) organized on the basis of following set of CTL formulas that characterize the control flow structure: different choreography compatibility classes  Sequence: A list of components to be defined and verifying deadlock free property. done in order. In [8] was developed a method for verifying  If-then-else: the selection based on temporal consistency in the Web Service flow. some obviously defined conditions. Time ontology is added tothe OWL-S  Choice: any of the given components specification, and then the annotated OWL-S is may be chosen for execution. transformed into formal model TCPN (Time  Repeat-while: the component is Constraint Petri Net), then temporal consistency performed repeatedly while certain of Web Service flow is verified. conditions are satisfied. In [9], the authors use a WS-CDL (Web Services  Repeat-until: the component is Choreography Description Language) performed repeatedly until some description of composite Web services, and conditions hold. define an operational semantics for a translation  Any-Order: the components are of a subset of WS-CDL into a network of Timed performed in some unspecified order but Automata. Uppaal tool is used for the validation not concurrently. and verification of the generated timed  Split: the components are activated and automata. performed concurrently. It can be seen that there is little work on timing  Split+Join: the parallel execution is constraint satisfiability based on formal methods synchronizing with barrier and which can combine semantic web approach. synchronization. On the other hand and to our knowledge, there is no research conducted on bounded liveness 3.2. Timing Constraint Specification property verification. In this paper, we propose a global methodology Based on Semantic Web, OWL-S describes the for specifying and verifying timed semantic web service semantic in different aspects. services. First, we use OWL-S ontology to Unfortunately, it still lacks the definition of time specify the web services. The Time-Entry constraints for Web Service which makes it ontology allows us to express temporal and difficult to verify temporal properties of the Web timed concepts. The resulting model is Service flow. transforming into a network of timed automata to To provide support for describing temporal be verified with Uppaal tool. properties for OWL-S, we use an (entry) sub- ontology of time, which is much simpler than the 2 full ontology of DAML-Time which provides the 3. TIMED SEMANTIC WEB SERVICES basic temporal concepts and relations that most SPECIFICATION simple applications would need i.e. instants and, 3.1. Owl-S Overview intervals [11]. By adding timing constraints to OWL-S, the time OWL-S (Web Ontology Language for Services) information related to the service can be defined is a high level ontology-based language for easily. The entry sub-ontology provides quick describing web service properties [10]. In this access to the essential vocabulary in OWL for language, each web service is specified in three the basic temporal concepts and relations. It XML-based parts: service profile, which covers relations among instants and intervals describes what the service does? Service and instant-like and interval-like events such as model, which describes how does the service "before" and "overlaps". It includes measures for work (behave); and service grounding, which durations, so that we can say a course will last 1 provides details on how to invoke a service through messages.OWL-S allows the 2 DAML-Time Homepage: description of the external behavior of a Web http://www.cs.rochester.edu/~ferguson/daml/ International Conference on Advanced Aspects of Software Engineering ICAASE, November, 2-4, 2014, Constantine, Algeria. 84 ICAASE'2014 Specification and Verification of Timed Semantic web Services hour and 30 minutes, and it also includes a clock Automata are extensions of finite state automata and calendar terms so that we can say a course with constraints on timing behavior. The starts at 10:00am on Monday, December 17, underlying finite state automata are augmented 2013. with a set of real time variables. These basic temporal constraint relations are: Definition1. Timed Automaton is a six-  Before (d₁, d₂): d₁ ends before d₂ starts and there is an interval between them. element tuple ( , , , , , ) where:  Meets (d₁, d₂): d₁ ends at the same  Σis a finite set of actions, instant when d₂ starts to execute.  is a finite set of locations,  Finishes (d₁, d₂): d₂ starts after d₁ starts  ⊆ is an initial location, and before d₁ ends, and d₂ ends at the  is a finite set of clocks, same instant with d₁.  ⊆ × × ×2 × ( ) is a  Overlaps (d₁, d₂): d₂ starts after d₁ starts transition relation, and before d₁ ends, and d₂ ends after d₁  is a (location) invariant. ends. Each element e of is denoted by 〈 , , , , 〉  Covers (d₁, d₂): d₁ execution interval represents a transition from the location to the includes d₁ execution interval. location ′, executing the action , with the set  Starts (d₁, d₂): d₂ starts at the same ⊆ of clocks to be reset, and with the clock instant with d₁, and d₂ ends after d₁ constraint defining the enabling condition for ends. .  Equals (d₁, d₂): d₂ starts and ends at the same instant with d₁. 4.2. Bounded liveness Notice that, an interval d may be also written as [b, e] corresponding to beginning and ending Temporal properties are conventionally point, respectively. classified into safety and liveness properties. A liveness property is a property, stating that "something good will eventually happen", e.g., 4. Timed Model Checking the program will terminate. Nevertheless, this still insufficient to ensure Model Checking [12] is one of the most correctness in case real-time deadlines must be successful approaches for verifying temporal specifications of hardware and software observed. In reality, we need to establish that systems. System properties are specified in the property in question will hold within a certain temporal logic for which various formalisms upper time-bound. Thus, a bounded liveness exist. Classically two types of properties are property is a liveness property that comes with a distinguished, safety and liveness. In practical maximal delay within which the "good thing" applications, safety properties are prevalent. must happen. Several versions are available. Consequently, very efficient algorithms and tools We consider the more efficient one. Based on have been developed for checking safety the method proposed in [15] in which time- properties. A model-checking tool accepts bounded leads-to properties are reduced to system designs (called models) and properties simple safety properties, first the model under (called specification) that models are expected investigation is extended with a boolean variable to satisfy. The tool then outputs yes, if the given and an additional clock . The boolean model satisfies given specifications and variable must be initialized to false. Whenever generates a counter example otherwise. starts to hold, is set to true and the clock is In this paper, we choose Timed Automata as reset. When commences to hold, is set to underlying model, and TCTL [13] logic to specify false. Thus the truth-value of b indicates whether the property to verify. there is an obligation of to hold in the future and measures the accumulated time since this 4.1. Timed automata unfulfilled obligation started. The time-bounded leads-to property ↝ , ⊆ ℝ is simply In this section we reply Timed Automata, which were introduced by Alur and Dill [14]. Timed International Conference on Advanced Aspects of Software Engineering ICAASE, November, 2-4, 2014, Constantine, Algeria. 85 ICAASE'2014 Specification and Verification of Timed Semantic web Services obtained by verifying the safety property∀□( ⇒ behavior of the (composite) service specified ≤ ). with service operation and time semantic Example: Intuitively, the formulae ↝[ , ] information. With Uppaal tool, verification of temporal property can be conducted. In the express that for all the runs, always when following, we describe both untimed and timed holds, holds in 2 to 3 units of time. InFigure 1, transformation rules from Timed OWL-S to the formula ⇒ ≤ holds for all states of one Timed Automata. run. If this is true for all other runs, then the formulae ↝[ , ] holds too. Sequence (P₁, P₂) Initial location is marked by a double circle. If Cond then P₁ else P₂ Figure 1Example of TCTL Formulae 4.3. Generic timed OWL-S verification approach The paper describes how to model Web Services and determine whether the specification satisfies the bounded liveness property. In the following we present the Split (P₁ , P₂) and Split-join (P₁ , P₂) Network different steps of the proposed approach: (set) of Timed Automata allows expressing the parallelism. Edges labeled with complementary  Step1: different web services are actions over the common channel Sync modeled in extended OWL-S language, synchronize.  Step2: automated composition is performed in respect of customer requirements,  Step3: transformation of the composed service specification along with its imposed timing constraints into Timed Automata model,  Step 4: specification of the formulae to Repeat P While Cond verify and augment Timed Automata with a necessary variable as explained We can also obtain Repeat-Until by replacing in section 4.2, by  Step 5: automatically verify the formula with Uppaal verifier,  Step 6: If the property is not satisfied go to Step 1 to correct the OWL-S Before (d₁, d₂) We use the clock to count time specification. for , ∈ {1,2}. The guard == ₁ 4.4. Timed OWL-S Timed Automata (respectively == ₁) marks the begin Transformation Rules (respectively the end) of ₁. The invariant ≤ ₁ (respectively ≤ ₁) forces the system Timed OWL-S is taken to specify logical structures, more important, temporal aspects of to leave once == ₁ (respectively == ₁). service processes with rich semantic Analogously for ₂. information. Transformed from the extended OWL-S process model, Timed Automata model is constructed to depict the structure and International Conference on Advanced Aspects of Software Engineering ICAASE, November, 2-4, 2014, Constantine, Algeria. 86 ICAASE'2014 Specification and Verification of Timed Semantic web Services Equals (d₁, d₂) Meets (d₁ , d₂) Overlaps (d₁, d₂) Since ₁ is not finished when 5. Case Study: Multimodal Transport ₂ starts, we use another clock to count for ₂. Thus, and allow to express parallelism. Multimodal transport is being used across a wide range of government, it is generally considered as the most efficient way of handling an international door to door transport operation. This is so because multimodal transport allows combining in one voyage the specific advantages of each mode, such as the flexibility of road haulage, the larger capacity of railways Finishes (d₁, d₂) and the lower costs of water transport in the best possible fashion. Multimodal transport also offers the shipper the possibility to rely on a single counterpart rather than having to deal with each and every modal specialist of the transport chain. While multimodal transport seems to offer only benefits to all parties, shippers and service providers, it is also very difficult to achieve. It Covers (d₁, d₂) requires a thorough control over all the steps involved in international transport; this means extensive use of information technologies that can provide freedom to plan and operate to carriers and reliable liability regimes to customers. In this case, we deal with the online shipment. Track-Ship is a fictitious service that offers Starts (d₁ , d₂) online tracking and helps customers to take an appropriate decision to change transport strategy when it is necessary. For example, the transport mode chosen may have to change over time when delays happen. So let's consider this hypothetical Scenario. The supposed itinerary combines sea and railway transport. The departure date is in 5 days from registration and the arrival is in 10 days. On arrival, if there is no administrative problem, the railway transport is in 1day and take 2days to arrive at International Conference on Advanced Aspects of Software Engineering ICAASE, November, 2-4, 2014, Constantine, Algeria. 87 ICAASE'2014 Specification and Verification of Timed Semantic web Services destination. The delay due to administrative Also, two other classes of Interval type are problem may take 2 days. In this case, customer created to describe intervals corresponding to has the choice to change to air transport or keep administrative procedure (AdminProcedure) and the previous plan, i.e.Sea-railway combined duration allowed to change transport strategy transport. A confirmation must be done no later (Change). than 1 to 2 days after shipment arrives in port, confirmation interval must be finished at the 5.2. Service Composition same instant as the interval corresponding to the administrative problem processing is finished. Now, it only remains for us the automated The airport departure is in 2 hours of composition based on customer needs. administrative problem solving and the air transit Specifically, different timed schedules time is not more than 1 hour. Finally, the goods betweenthese intervals are met. For example, are in stock within 1 day of arrival. the temporal relation between ProcessTimeSea and AdminProcedure is constructed by the use 5.1. Modeling Temporal Behavior of a restriction on the object property intMeets i.e. the expression "intMeets only The Track-Ship is a composite service. It AdminProcedure" to ProcessTimeSea class. We contains three main services i.e. Sea, Railway apply the same logic to the rest of the intervals. and Air Services, each of them allows us to search information about available itineraries corresponding to our preferred needs. For example, the Air one is a service that makes it easy to find flights that meet our needs and planning travel. It includes a sequence of three operations i.e. GetDesiredDetails, SelectAvailableItinerary and Reservation. These three services are performed in parallel from which we use the control constraint "split" for the composition. The OWL-S specification remains insufficient to describe adequately our scenario since the timed aspects are not taking account. For this purpose we add two output parameters: WaitTime, that specifies the time between reservation instant and departure instant, and ProcessTime, that specifies the time between departure instant and arrival instant. It makes easy with the use of the entry sub- ontology of time; ProcessTime and WaitTime are defined as Intervals. To schedule the three Figure 3 AdminProcedure OWL Code itineraries we need to create ProcessTime and WaitTime subclasses corresponding to sea, Figure 3shows the entire description of the class railway and air information. AdminProcedure. International Conference on Advanced Aspects of Software Engineering ICAASE, November, 2-4, 2014, Constantine, Algeria. 88 ICAASE'2014 Specification and Verification of Timed Semantic web Services Now, we need to ensure the correctness of  In red, corresponds to the worst case the composed service i.e. goods are in where a customer chooses to keep the stock within a fixed period of time for this initial plan, i.e. sea-railway combined Figure 4 Generated Timed Automaton case. In the following, we try to verify the transport in spite of delays. property: "Goods are in stock within 19 days 5.4. Formal Verification and 3 hours (i.e. 459 hours) from registration". Corresponding to [16], to specify the property to verify, the model under investigation must be 5.3. From timed OWL-S to timed automata extended with a boolean variable b and an additional clock Elapsed. The boolean variable b By applying transformation rules presented in must be initialized to false. Whenever Section 3.4, the Timed Automata is generated from Registration is made, b is set to true and the the OWL-S specification. The generated Timed clock Elapsed is reset. When the goods arrive, b Automaton is presented in 4. We can easily is set to false. Thus the property “Goods are in distinguish three main runs: stock within 19 days and 3 hours (i.e.  In green, the succession of actions 459 hours) from registration” is obtained by corresponds to the sea-railway verifying the safety property combined transport case; ∀□(b⇒Elapsed≤459)  In orange, it corresponds to the situation where a customer chooses to change 5.4.1. Uppaal verifier results the transport strategy, to sea-air combined transport, in order to overtake The verifier shows that the formula is not lost time due to an administrative satisfied Hence, the selected travels cannot be problem; accepted. International Conference on Advanced Aspects of Software Engineering ICAASE, November, 2-4, 2014, Constantine, Algeria. 89 ICAASE'2014 Specification and Verification of Timed Semantic web Services 5.4.2. Uppaal simulator [1] ter Beek, Maurice and Bucchiarone, Antonio and Gnesi, Stefania. A Survey on Service Composition The simulator allows us to views the counter Approaches:From Industrial Standards to Formal example. In our case, it indicates the run Methods. Technical Report 2006-TR-15. 2006 corresponding to the situation when users [2] Khadka, R., & Sapkota, B. An evaluation of dynamic choose to keep the first plan in spite of the web service composition approaches. [ed.] SciTePres. 2010. delays. [3] Diaz, G., Pardo, J. J., Cambronero, M. E., Valero, V., Also, the simulator allows us to explore variable & Cuartero, F. Automatic translation of ws-cdl choreographies to timed automata . Formal valuations (Figure 6). For example, when goods Techniques for Computer Systems and Business arrive by tracing the previous run, the clock Processes. 2005, pp. 230-242. Elapsed is in [456;480] and violate the condition [4] Kazhamiakin, R., Pandya, P., et Pistore, M. Web Elapsed≤459. The lower bound of the interval Service Compositions. Engineering Service corresponds to the arrival time at the airport and Compositions. 2005, p. 59. the upper bound corresponds to the time in [5] Chaochen, Z., Hoare, C. A. R., & Ravn, A. P. A which goods are available in stock. Moreover, calculus of durations. [ed.] Elsevier. 5, 1991, the clock x counts time in which goods should Information processing letters, Vol. 40, pp. 269-276. [6] Dong, J. S., Liu, Y., Sun, J., & Zhang, X. Verification be in stock after arriving. Contrariwise, the clock of computation orchestration via timed automata. y is used to specify that the end of the Formal Methods and Software Engineering. 2006, pp. confirmation interval (i.e. [24,48]) must 226-245. correspond to the administrative problem [7] Guermouche, N., & Godart, C. Timed conversational resolution (i.e. [0,48]). Formally expressed as protocol based approach for web services analysis. Finishes([0,48],[24,48]) used to the entry sub- Service-Oriented Computing. 2010, pp. 603-611. ontology of time. [8] Liu, R., Hu, C., Zhao, C., & Gao, Z. Verification for time consistency of Web service flow. Computer and Information Science. May 2008, pp. 624-629. 6. Conclusion And Future Work [9] Emilia Cambronero, M., Díaz, G., Valero, V., & Martínez, E. Validation and verification of Web This paper proposes a verification methodology services choreographies by using timed automata. 1, for temporal properties of Semantic Web Service 2011, Journal of Logic and Algebraic Programming, Vol. 80, pp. 25-49. by Uppaal model checker. Taking account of [10] Martin, D., Paolucci, M., McIlraith, S., Burstein, M., time information, we use entry sub-ontology of McDermott, D., McGuinness, D., ... & Sycara, K. time in conjunction with OWL-S for describing Bringing semantics to web services: The OWL-S the temporal content of Web Services. Then we approach. [ed.] Springer. Semantic Web Services and transform the OWL-S specification into Timed Web Process Composition. 2005, pp. 26-42. Automata, which is mandatory for an automated [11] Hobbs, J. R., & Pan, F.An ontology of time for the verification of Web Services. Transformation semantic web. [ed.] ACM. 1, 2004, ACM Transactions on Asian Language Information rules are projected and a case study is Processing (TALIP), Vol. 3, pp. 66-85. presented to show the applicability of our [12] Bérard, B., Bidoit, M., Finkel, A., Laroussinie, F., approach. Petit, A., Petrucci, L., & Schnoebelen, P. Systems and software verification: model-checking techniques and In future work, we aim to automate our proposed tools. 2010. approach with a use of Model-Driven [13] Alur, R., Courcoubetis, C., & Dill, D. Model-checking Engineering (MDE) tools for implementing in dense real-time. 1993. pp. 2-34. transformation rules from Timed OWL-S [14] Alur, R., Dill, D. L. A theory of timed automata. ontology to Timed Automata model. In addition, Theoretical computer science . 1994. pp. 183-235. we will extend the applicability of our approach [15] Lindahl, M., Pettersson, P., & Yi, W. Formal design to verify more properties. Finally, we also plan to and analysis of a gear controller. [ed.] Springer. Tools and Algorithms for the Construction and Analysis of verify more ambitious applications. Systems. 1998, pp. 281-297. [16] Boumaza, A., Maamri, R. Bounded liveness in 7. REFERENCES semantic web services. ACIT. December 2012, 13, pp. 602-610. International Conference on Advanced Aspects of Software Engineering ICAASE, November, 2-4, 2014, Constantine, Algeria. 90