=Paper=
{{Paper
|id=Vol-1294/paper9
|storemode=property
|title=Specification and Verification of Timed Semantic web Services
|pdfUrl=https://ceur-ws.org/Vol-1294/paper9.pdf
|volume=Vol-1294
|dblpUrl=https://dblp.org/rec/conf/icaase/BoumazaM14
}}
==Specification and Verification of Timed Semantic web Services==
https://ceur-ws.org/Vol-1294/paper9.pdf
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