Article Preview
TopIntroduction
Service Oriented Architecture (SOA) provides standard for interoperating different software applications, running on heterogeneous platforms and/or frameworks. Actually, SOA has received a great deal of attention and is becoming an attractive solution for enterprise information systems.
Simultaneously, major effort has been undertaken to transform the actual Web, from distributed documents to a structure of interlinked resources, whose semantic is explicitly defined due to ontologies. Changing the way of using the Web has a clear impact on Web services. These services, which were formerly used through form-based Web pages, can now, be described in a machine-interpretable form enabling automation of many tasks currently performed by human-being. In literature, we can find a variety of ontology-based language for describing various aspects of Web services: OWL-S, WSMO and SAWSDL are the most important approaches (Wang, Gibbins, Payne, Patelli, & Wang, 2015).
In the field of Web services, there is an increasing realization that temporal information plays a crucial role such as timeouts, durations, dates and times. The simplest way approach to specify time in semantic Web services is to simply use an ontology of time which can be able to help for managing time of real world services. However, this approach has several limitations: (1) It would be the programmer’s decision to encode manually temporal information and anchor them to events. Hence, there are many ways to encode the same scenario, that’s why the automation of the information retrieval and exploitation process often fails. For example, begin and end event’s time (a flight time) can be encoded as inputs parameters (arrival and departure times) but also can be encoded as temporal information anchored to events encoded as inputs parameters (arrival and departure events) (2) the type of semantics given to ontology-based work tends to be structural rather than behavioural oriented. As a result the semantics developed for OWL-S, are still deficient in automatic verification of Web services properties such as temporal ones and even for the simplest ones as deadlock free (3) complex time expressions may be specified by using temporal information (such as durations, timeouts,…) but it may leads to inconsistencies due to increasing complexity that's why, it is important to provide ways to ensure correctness of behavior of a service with respect to relevant quantitative temporal properties. For example, arrival date should be at least one day before departure date in the case of a hotel booking, apartments can be rented only for periods longer than one months. The shipments must be delivered no later than 24 hours after the customer request.
In this paper, researchers address the limitations elucidated overhead through a novel approach to automate Web service verification of both temporal qualitative and quantitative properties for timed semantic Web services, which combines ontology of Web services, ontology of time and formal methods. Our approach covers both the specification of temporal information using an existed sub entry ontology of time (Pan & Hobbs, 2004) and formal verification through the mapping of the augmented specification of Web services by quantitative temporal information into timed automata. The contributions of this work are three-fold: First, researchers present generic pattern to better facilitate specification of temporal information on processes in OWL-S ontology and avoid ambiguity by adding new classes (i.e. process time and deadline classes). Second, researchers define a set of mapping rules to automatically encode various control constructs and temporal information defined in OWL-S into timed automata. The latter is equipped with a formal semantic which allow automatic verification of both kinds of temporal properties i.e. qualitative and quantitative properties. Third, researchers show how to use UPPAAL checker for model checking required properties formulated in Timed Computation Tree Logic (TCTL) (Alur, Courcoubetis, & Dill, 1993).
The remainder of the paper is organized as follows. Section 2 highlights related work about proposed techniques and methods about formal verification of temporal properties on Web services. Section 3 sketches the models used in our approach namely OWL-S ontology and timed-automata. Section 4 defines the set of rules for automating translation from OWL-S description to timed automata network and show how it allows formal verification of temporal properties i.e. safety, liveness and bounded liveness property. Section 5 shows a case study analysis to demonstrate the use of our approach in applications. Finally, Section 6 concludes the work.