- 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.
Automatic composition is the capability to automatically compose a set of services to fulfill user requirements when a single service is not available for fulfilling these requirements. Composing services need an approach based on semantic descriptions, as the requester required functionally has to be expressed in a high-level and abstract way to enable reasoning procedures.
Efficiently, the semantic web community allows reasoning about web resources by explicitly declaring their preconditions and effects with terms defined precisely in ontologies.
Furthermore, in Semantic Web Services, the common need for temporal information is satisfied by the use of the temporal ontologies to allow using of temporal concepts. However, the complexity comes usually with the growing expressiveness; it becomes a challenging area to ensure correctness. Hence, the verification of Web Service flow becomes more and more important.
Formal methods are particularly well appropriate
to address most of the aforementioned issues
(e.g. composition and correctness). The majority
of these are based on state-action models (e.g.
labeled transition systems, timed automata, and
Petri nets) or process models (e.g. π-calculus
and other calculi) [
Recently, a diversity of concrete proposals from
the formal methods community have emerged in
order to verify the correctness of the web service
composition which is based on state action
models or process models [
In [
In [
In [
In [
In [
It can be seen that there is little work on timing constraint satisfiability based on formal methods and which can combine semantic web approach. On the other hand and to our knowledge, there is no research conducted on bounded liveness property verification.
In this paper, we propose a global methodology for specifying and verifying timed semantic web services. First, we use OWL-S ontology to specify the web services. The Time-Entry ontology allows us to express temporal and timed concepts. The resulting model is transforming into a network of timed automata to be verified with Uppaal tool.
OWL-S (Web Ontology Language for Services)
is a high level ontology-based language for
describing web service properties [
Composite processes are used to describe collections of processes (either atomic or composite) organized on the basis of following control flow structure: Sequence: A list of components to be done in order. If-then-else: the selection based on some obviously defined conditions. Choice: any of the given components may be chosen for execution. Repeat-while: the component is performed repeatedly while certain conditions are satisfied. Repeat-until: the component is performed repeatedly until some conditions hold. Any-Order: the components are performed in some unspecified order but not concurrently. Split: the components are activated and performed concurrently. Split+Join: the parallel execution is synchronizing with barrier synchronization.
Based on Semantic Web, OWL-S describes the service semantic in different aspects. Unfortunately, it still lacks the definition of time constraints for Web Service which makes it difficult to verify temporal properties of the Web Service flow.
To provide support for describing temporal
properties for OWL-S, we use an (entry)
subontology of time, which is much simpler than the
full ontology of DAML-Time2 which provides the
basic temporal concepts and relations that most
simple applications would need i.e. instants and,
intervals [
By adding timing constraints to OWL-S, the time information related to the service can be defined easily. The entry sub-ontology provides quick access to the essential vocabulary in OWL for the basic temporal concepts and relations. It covers relations among instants and intervals and instant-like and interval-like events such as "before" and "overlaps". It includes measures for durations, so that we can say a course will last 1 2DAML-Time Homepage: http://www.cs.rochester.edu/~ferguson/daml/ hour and 30 minutes, and it also includes a clock and calendar terms so that we can say a course starts at 10:00am on Monday, December 17, 2013.
These basic temporal constraint relations are: Before (d₁, d₂): d₁ ends before d₂ starts and there is an interval between them. Meets (d₁, d₂): d₁ ends at the same instant when d₂ starts to execute. Finishes (d₁, d₂): d₂ starts after d₁ starts and before d₁ ends, and d₂ ends at the same instant with d₁. Overlaps (d₁, d₂): d₂ starts after d₁ starts and before d₁ ends, and d₂ ends after d₁ ends. Covers (d₁, d₂): d₁ execution interval includes d₁ execution interval. Starts (d₁, d₂): d₂ starts at the same instant with d₁, and d₂ ends after d₁ ends. Equals (d₁, d₂): d₂ starts and ends at the same instant with d₁.
Notice that, an interval d may be also written as [b, e] corresponding to beginning and ending point, respectively.
Model Checking [
In this section we reply Timed Automata, which
were introduced by Alur and Dill [
Definition1. Timed Automaton is a sixelement tuple ( , , , , , ) where: Σis a finite set of actions, is a finite set of locations, ⊆ is an initial location, is a finite set of clocks, ⊆ × × × 2 × ( ) is a transition relation, is a (location) invariant.
Each element e of is denoted by 〈 , , , , 〉 represents a transition from the location to the location ′ , executing the action , with the set ⊆ of clocks to be reset, and with the clock constraint defining the enabling condition for .
Temporal properties are conventionally classified into safety and liveness properties. A liveness property is a property, stating that "something good will eventually happen", e.g., the program will terminate.
Nevertheless, this still insufficient to ensure
correctness in case real-time deadlines must be
observed. In reality, we need to establish that
the property in question will hold within a certain
upper time-bound. Thus, a bounded liveness
property is a liveness property that comes with a
maximal delay within which the "good thing"
must happen. Several versions are available.
We consider the more efficient one. Based on
the method proposed in [
Example: Intuitively, the formulae ↝ [ , ] express that for all the runs, always when holds, holds in 2 to 3 units of time. InFigure 1, the formula ⇒ ≤ holds for all states of one run. If this is true for all other runs, then the holds too. behavior of the (composite) service specified with service operation and time semantic information. With Uppaal tool, verification of temporal property can be conducted. In the following, we describe both untimed and timed transformation rules from Timed OWL-S to Timed Automata.
Sequence (P₁, P₂) Initial location is marked by a double circle.
(set) of Timed Automata allows expressing the parallelism. Edges labeled with complementary actions over the common channel Sync synchronize.
Repeat P While Cond We can also obtain Repeat-Until by replacing by Before (d₁ , d₂ ) We use the clock to count time for , ∈ {1,2}. The guard == ₁ (respectively == ₁ ) marks the begin (respectively the end) of ₁ . The invariant ) forces the system ≤ ₁ (respectively ≤ ₁ to leave once == ₁ (respectively Analogously for ₂. == ₁). Meets (d₁ , d₂) Overlaps (d₁ , d₂) Since ₁ is not finished when ₂ starts, we use another clock to count for ₂. Thus, and allow to express parallelism.
Covers (d₁ , d₂ ) Starts (d₁ , d₂) Equals (d₁ , d₂)
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 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 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 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 destination. The delay due to administrative problem may take 2 days. In this case, customer has the choice to change to air transport or keep the previous plan, i.e.Sea-railway combined transport. A confirmation must be done no later than 1 to 2 days after shipment arrives in port, confirmation interval must be finished at the same instant as the interval corresponding to the administrative problem processing is finished. The airport departure is in 2 hours of administrative problem solving and the air transit time is not more than 1 hour. Finally, the goods are in stock within 1 day of arrival.
The Track-Ship is a composite service. It contains three main services i.e. Sea, Railway 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 subontology of time; ProcessTime and WaitTime are defined as Intervals. To schedule the three itineraries we need to create ProcessTime and WaitTime subclasses corresponding to sea, railway and air information.
Also, two other classes of Interval type are created to describe intervals corresponding to administrative procedure (AdminProcedure) and duration allowed to change transport strategy (Change).
Now, it only remains for us the automated composition based on customer needs. Specifically, different timed schedules betweenthese intervals are met. For example, the temporal relation between ProcessTimeSea and AdminProcedure is constructed by the use of a restriction on the object property intMeets i.e. the expression "intMeets only AdminProcedure" to ProcessTimeSea class. We apply the same logic to the rest of the intervals. Now, we need to ensure the correctness of the composed service i.e. goods are in stock within a fixed period of time for this
In red, corresponds to the worst case where a customer chooses to keep the initial plan, i.e. sea-railway combined case. In the following, we try to verify the property: "Goods are in stock within 19 days and 3 hours (i.e. 459 hours) from registration".
By applying transformation rules presented in Section 3.4, the Timed Automata is generated from the OWL-S specification. The generated Timed Automaton is presented in 4. We can easily distinguish three main runs: In green, the succession of actions corresponds to the sea-railway combined transport case; In orange, it corresponds to the situation where a customer chooses to change the transport strategy, to sea-air combined transport, in order to overtake lost time due to an administrative problem; transport in spite of delays.
Corresponding to [
The verifier shows that the formula is not satisfied Hence, the selected travels cannot be accepted.
The simulator allows us to views the counter example. In our case, it indicates the run corresponding to the situation when users choose to keep the first plan in spite of the delays.
Also, the simulator allows us to explore variable valuations (Figure 6). For example, when goods arrive by tracing the previous run, the clock Elapsed is in [456;480] and violate the condition Elapsed≤459. The lower bound of the interval corresponds to the arrival time at the airport and the upper bound corresponds to the time in which goods are available in stock. Moreover, the clock x counts time in which goods should be in stock after arriving. Contrariwise, the clock y is used to specify that the end of the confirmation interval (i.e. [24,48]) must correspond to the administrative problem resolution (i.e. [0,48]). Formally expressed as Finishes([0,48],[24,48]) used to the entry subontology of time.
This paper proposes a verification methodology for temporal properties of Semantic Web Service by Uppaal model checker. Taking account of time information, we use entry sub-ontology of time in conjunction with OWL-S for describing the temporal content of Web Services. Then we transform the OWL-S specification into Timed Automata, which is mandatory for an automated verification of Web Services. Transformation rules are projected and a case study is presented to show the applicability of our approach.
In future work, we aim to automate our proposed approach with a use of Model-Driven Engineering (MDE) tools for implementing transformation rules from Timed OWL-S ontology to Timed Automata model. In addition, we will extend the applicability of our approach to verify more properties. Finally, we also plan to verify more ambitious applications.