=Paper=
{{Paper
|id=Vol-1294/paper3
|storemode=property
|title= Mop-ECATNets for Formal Modeling Dynamic Web Services
|pdfUrl=https://ceur-ws.org/Vol-1294/paper3.pdf
|volume=Vol-1294
|dblpUrl=https://dblp.org/rec/conf/icaase/LatrecheB14
}}
== Mop-ECATNets for Formal Modeling Dynamic Web Services==
https://ceur-ws.org/Vol-1294/paper3.pdf
ICAASE'2014 Mop-ECATNets for Dynamic Web Services Formal Modeling
Mop-ECATNets for Dynamic Web
Services Formal Modeling
FATEH LATRECHE FAIZA BELALA
LIRE laboratory, Constantine 2 University LIRE laboratory, Constantine 2 University
Constantine, Algeria Constantine, Algeria
fateh_lat@yahoo.fr faiza.belala@univ-constantine2.dz
Abstract – Mop-ECATNets are a sound combination of Meta Petri Nets and OpenECATNets (Open
Extended Concurrent Algebraic Term Nets). They inherit fl exibility of control from Meta nets and
data structure, concurrency and composability from Open-ECATNets. Our aim in this work is to show
how Mop-ECATNet, a layered Petri nets based model, makes it possible the formal execution and
analysis of dynamic web services at design time. We argue that it is possible and valuable to provide a
real-time rewriting logic based model that accounts for failure events and recovery actions. In order to
illustrate its potential, we apply our approach through a detailed case study of a traveler map dynamic
service.
Keywords – Dynamic Web services, Open-ECATNets, Meta Petri nets, real-time rewriting logic
Algebraic Term Nets) to enhance design and
analysis of dynamic Web services. Mop-
1. INTRODUCTION ECATNets are an extended version of Open-
ECATNets [3], allowing the formal specifi cation
Service Oriented Architecture (SOA) is a of failure events and recovery actions.
development model aiming at raising integration
and interoperability of software components. In Since their introduction, by Carl Adam Petri
SOA services are units of work, they are self- [4] in the beginning of sixties, Petri nets have
describing modular applications that can be been successfully applied through their
published, localized and invoked across the web extensions as a foundation for software systems
thanks to a set of XML standards. In most cases addressing many challenging issues. In
elementary services cannot carry out required particular, Meta Petri nets [5] as multi-level Petri
functionalities. Thus, we need invoking several net model have been proposed for modeling
Web services and then composing them in order dynamic processes and their control. Also,
to reach new personalized, rich and more Open-ECATNets have been proposed to tackle
interesting functionalities. various aspects of Web service compositions,
such as semantic compatibility of exchanged
Several efforts on web service modeling and messages, functional compatibility and service
analysis have already been done by researchers refi nement. Open-ECATNets benefi t from their
and industrial practitioners. But, mostly these defi nition in term of rewriting logic.
works pay less attention to dynamic features.
Also, current Web service standards and Rewriting logic is a general framework, in
languages provide limited constructs for which not just applications, but entire formalisms
specifying exceptional behavior [1] [2], and they and computation models can be naturally
are semi-formal requiring translation to generate expressed. This logic allows correct reasoning on
formal models that admit checking. concurrent systems behavior. Several practical
languages were invented on the basis of
In this work, we propose using Mop- rewriting logic, the most known is Maude (SRI
ECATNets (Meta Open Extended Concurrent
International Conference on Advanced Aspects of Software Engineering
ICAASE, November, 2-4, 2014, Constantine, Algeria. 27
ICAASE'2014 Mop-ECATNets for Dynamic Web Services Formal Modeling
laboratory, United States)[6], a declarative functions selected by a context function. In this
language where several concurrent applications work a Meta transitional Petri net having two
have been considered. Furthermore, various layers is used. The lower layer contains the
extensions of rewriting logic and Maude were service net and the control layer contains one or
made in order to provide additional more Meta control nets. This proposal is very
representation and reasoning abilities. Real-Time promising, but it suggests using ordinary Petri
Maude is one of these extensions [7], used for nets in both basic and control layers. This
specifying and analyzing real-time and dynamic remains inappropriate for modeling real-time and
systems. dynamic constraints. Also, the proposed
composition approach is lacking implementation
The remainder of this paper is organized as details.
follows. In section 2, we give an overview of
related works. Sections 3 and 4 introduce the Our approach for specifying and analyzing
real-time rewriting logic and Open-ECATNets dynamic Web services is quite different, since it
model. In Section 5, we deal with the Mop- uses useful features of many Petri nets models
ECATNets model for dynamic Web services. We and it’s based on a unique semantic framework:
identify its integration in real-time rewriting logic real-time rewriting logic. Mop-ECATNets are also
semantic framework, so both structural and executable; they are able to reconfi gure
behavior aspects are considered. In section 6, dynamically their structure. Thus, services
we illustrate our formalization approach by failures are conditions that trigger adaptation
means of a realistic case study, the traveller map actions. Besides, our developed model allows
dynamic service. We also show how some formal checking of some inherent properties
relevant properties are formally checked. The related to dynamic Web services thanks to the
paper is outlined by some concluding remarks Real Time Maude model checker tool.
and perspectives.
2. RELATED WORK
3. REAL-TIME REWRITING LOGIC
Several attempts [08] [09] [10] have already
been conducted to formalize web services but, The objective of this section is to present
without taking into account their dynamic elementary concepts of real-time rewriting logic
features such as, changes of user profile, for more details, reader can refer to [6] [7] [13].
invocation context and quality of services. In this Since its introduction, rewriting logic has
section, we situate our work regarding some attracted the interest of both theorists and
theoretical and architectural models dealing with practitioners. Its experimentation through many
dynamic issue of web services. applications has conducted to propose some
Authors of [11] have given a Petri net based extensions of this logic. The most signifi cant one
is the real-time rewriting logic allowing
methodology for context aware services design.
Thus, context aware Web service is defi ned by a specifi cation of real-time systems. Basic
Petri net, where places represent sensed/inferred specifi cation elements of real-time rewriting logic
context concepts and transitions represent the are real-time rewrite theories [14]. Rewriting rules
actions. The advantage of this work is the well of a real-time rewrite theory are of two kinds: I R
description of context aware applications and its and TR, IR is a set of instantaneous rewrite rules,
possible integration within dynamic environment and TR is a set of tick rewrite rules.
thanks to contextual information. But, this Real-Time Maude is an extension of Maude.
approach makes only use of fi rst-order logic It emphasizes ease and generality of
predicate formalism to specify context concepts. specifi cation, including support for distributed
This makes dynamic web services models quite real-time object based systems. Also, it provides
restrictive. a large range of simulation and analysis
In a similar work [12], Dmytro Zhovtobryukh techniques. This tool complements other real-
defi nes also a context aware Web service time analysis tools not only by the full generality
framework composed of two stages: planning of the specifi cation language and the range of
and composition reconfi guration. According to analysis techniques, but also by its simplicity and
this work, a context aware Web service is clarity. Real-time and hybrid systems are
defi ned as a complex functional unit having an represented as real-time rewrite theories, where
explicit inputs and outputs; it is also able to equations are used to specify data types and
perform two or more mutually exclusive service rewrite rules to mechanize dynamic and real-time
behavior.
International Conference on Advanced Aspects of Software Engineering
ICAASE, November, 2-4, 2014, Constantine, Algeria. 28
ICAASE'2014 Mop-ECATNets for Dynamic Web Services Formal Modeling
The main form of formal analysis consists in
simulating system behaviors by using the timed
rewriting commands. Besides, to gain more
assurance about a system, designer can use
timed search and timed linear temporal logic Figure 1 Graphical representation of ECATNet
model checking to explore many concurrent
behaviors of a system [14]. To make ECATNets able to model open
systems capable to interact with their
4. OPEN-ECATNets PRESENTATION environment, we have, in a previous work [3],
enriched their model by additional structures,
In addition to the use of rewriting logic in inspired from the open net model [10]. In
specifi cation of concurrent and distributed particular, Open-ECATNets are endowed with
system semantics, it is also a promising logical some open places representing the service
framework in which many logics and concurrency interaction points with environment. Formally
models as ECATNets [15] may be naturally their defi nition is as follows:
represented and interrelated. ECATNets are high
level algebraic Petri nets initially proposed by Definition 2. An Open-ECATNet : {E, Mi, Mf} is
Bettaz and Maouche [15]. They combine a particular marked ECATNet E : (P, T, sort, IC,
expression power of Petri nets and abstract data DT, CT, TC), such that:
types. By using ECATNets, we do not only gain
highly condensed system model, but we reach • P = IO ∪ ST, where IO is a set of
also an attractive theoretical model according to (Input/Output) places having a well defi ned
their simplicity and intrinsic concurrent nature. In sort and ST is a set of state places,
an ECATNet, transitions, places and arcs are • Mi and Mf are respectively the set of initial and
labeled by elements of the multi-set (noted as:
the fi nal markings such that: ∀ p ∊ IO, Mi(p)=
MTΣ /EUA(X)) of algebraic terms belonging to a
given algebra TΣ /EUA(X). Mf(p)=0.
Definition 1. An ECATNet (see Fig. 1) is a In an Open-ECATNet, the set of interface
high level Petri net having the structure (P, T, places (IO) are designed to defi ne external
sort, IC, DT, CT, TC), where: interaction and the set of state places (ST) to
model services states.
• P and T are respectively fi nite sets of places
Open-ECATNet (or ECATNet) behavior is
and transitions (with P∩ T=ø ); defi ned by way of concurrent computations in
• sort: P→ S is a function that associates to rewriting logic. Each transition is materialized by
each place an algebraic sort s of Σ ; a local rewriting rule of a given rewrite theory
• IC (Input Condition):P×T→ MTΣ /EUA(X), is a defi ning the distributed structure of ECATNet
function that specifi es partial conditions on states.
input place markings;
• DT (Destroyed Tokens): P× T → MTΣ /EUA(X), is 5. OPEN-ECATNets EXTENSION
another function that associates to each input
arc (p×t) of transition t, a multi-set of algebraic Because of their size and complexity,
terms to be consumed from input place; distributed and dynamic systems, as Web
• CT (Created Tokens): P× T→ MTΣ /EUA(X) services, may not be easily modeled. They
associates to each output place of P, a require using more tailored formalisms. Dynamic
multiset of algebraic terms which may be web services are highly affected by time. A
added when a transition is fi red; rigorous approach to tackle failures is to fix a
• TC (Transition Condition) is an additional maximal waiting time before launching
condition, when it is omitted, the default value adaptation process. The objective of this section
is to present the Mop-ECATNets model,
is the term true. designated to better specify and analyze
dynamic Web services.
A distinctive characteristic of ECATNets is
their strength in modeling synchronization To allow a flexible modeling of complex
constraints and complex system data structures. dynamic Web service process, we enhance
Open-ECATNets with the Meta Petri nets
They have been largely applied in modeling and
features [5]. In Meta Petri nets places,
checking various kinds of systems [16] [17] [18]. transitions, links and tokens of a lower level are
International Conference on Advanced Aspects of Software Engineering
ICAASE, November, 2-4, 2014, Constantine, Algeria. 29
ICAASE'2014 Mop-ECATNets for Dynamic Web Services Formal Modeling
active (available), if and only if their meta place
contains at least one token.
The Mop-ECATNets model is based on an
extension of two level Meta transitional nets
where Meta places control lower level transitions.
More precisely, each transition (send or receive
action) of the lower level is active regarding
tokens of Mop-ECATNets lower level
(exchanged messages), if and only if the
transition meta place contains the same token.
Mop-ECATNets are also equipped with timing
constraints: On one hand, all lower level
transitions are forced to fi re when they are
enabled; fi ring in this case is an atomic action.
On the other hand, some state places are
constrained by timestamp. This allows specifying
the requests adaptation timers (i.e. modeling the
fact that requested functionalities may be failed if Figure 2 A Mop-ECATNet example
elapsed time after the sending request action is
equal to a fi xed maximum delay). Formally, the ACTIV-TRANS (Fig. 3 to Fig. 5) are designed to
Mop-ECATNet defi nition is given by: implement our Mop-ECATNets model. The
Figure 3 shows a slightly modifi ed version of the
Defi nition 3. A Mop-ECATNet ME =< E, O, timed Maude module TOKENS that represent
Q, λ> is a two levels Meta transitional net having tokens abstract data types. In this module, we
as higher level net the marked ECATNet E and fi rstly import the predefi ned module NAT-TIME-
as lower level the Open-ECATNet O. Q is the DOMAIN-WITH-INF defi ning the time domain to
incidence function mapping meta places of E to be the natural numbers with the infi nity value.
transitions of O and λ: ST → N is a function that Then, we declare a set of sort and subsort
maps each state place (belonging to ST) to its relations useful to describe statically Mop-
reconfi guration timer. ECATNet tokens (a multi-set of algebraic terms
having the form tkid, tkid[t], where tkid is the
Let’s recall that: E = (P’, T’, sort’, IC’, DT’, CT’,
token identifi er and t represent the container
TC’) and O = {(IO∪ST, T, sort, IC, DT, CT, TC), place reconfi guration timer).
Mi, Mf}. In Fig. 2, we give a Mop-ECATNet,
where places mpt and mpt’ are the meta places Mop-ECATNets Marking is then formalized by
relative to transitions t and t’ of the lower Open- the timed module MARKING-SPEC (Fig. 4).
ECATNet. The Mop-ECATNet of this fi gure can According to our formalization, markings are
also be defi ned by the following sets: P’= {mpt, viewed as multi-sets of ordinary places, Meta
mpt’ }, T’= {mt}, Q = {(mpt, t), (mpt’, t’)}, IO = {pi, places, ordinary transitions and Meta transitions
pi’ }, ST = {p1, p2, p3},Mi = {(1, 0, 0)} , Mf = {(0, (operations declared in lines 6, 7, 8 and 9 of Fig.
1, 0), (0, 0, 1)} and λ= {(p3, 3)}. 4). Let’s note that in the case of transition, its
algebraic term must have the form < t, r >, where
5.1. Mop-ECATNets Semantics t is the name of transition and r is its timer value.
Our formalization of a Mop-ECATNet is based The third timed module ACTIV-TRANS (Fig.
on the following idea: a net marking is 5) defi nes, thanks to a set of equations, in which
considered as a multi-set of algebraic terms case a given transition is active regarding a
modeling places and its transitions as a multi-set particular token (the send or receive action is
of rewriting rules. In order to mechanize enabled for a particular exchanged message).
instantaneous fi ring of transitions, we add a timer For Mop-ECATNets model, it is worth noting
for each transition t belonging to T U T’. This that formalized services may be extended to
timer has either the value 0 to denote forced to model new Web service composition concepts,
fi re transitions, or the value INF (infi nity) for non and will make easy their interconnection with
fi rable transitions. services of other applications in the context of
Thus, Mop-ECATNets are defi ned in terms of heterogeneous systems. Also, time which is
timed rewrite theories. Three timed Maude currently an important aspect of Web services, is
modules TOKENS, MARKING-SPEC and straightforwardly modeled thanks to real-time
extension of Maude. Furthermore, checking
International Conference on Advanced Aspects of Software Engineering
ICAASE, November, 2-4, 2014, Constantine, Algeria. 30
ICAASE'2014 Mop-ECATNets for Dynamic Web Services Formal Modeling
Mop-ECATNets specifi cations is now possible These rules model fi ring of Mop-ECATNets
thanks to the Real Time Maude analysis tools. transitions when their timers have the value 0. As
results of fi ring, some tokens are removed from
tmod TOKENS is defi nite places and added to other places,
including NAT-TIME-DOMAIN-WITH-INF. transition timers are turned off (fi xed to the
sorts Token Token. infi nity value), and the function recomputeTimers
subsort Token Nat < Tokens. is applied to the entire resulting state to
subsort TkId < Token.
op _`[_`] : TkId Time -> Token [ctor prec 21].
recompute all transition timer values. Particularly,
op __ : Tokens Tokens -> Tokens [ctor assoc comm prec 22 this function tests if a transition is enabled, then
id: none ]. its timer is reinitialized to the value 0, otherwise
op none : -> Tokens [ctor]. the timer is left unchanged. More precisely, for
endtm each transition of a generic Mop-ECATNet (see
Fig. 6) we associate a rewriting rule having the
following interpretation:
Figure 3 Tokens of a Mop-ECATNet
• The rewriting rule associated to send-req
tmod MARKING-SPEC is
1 including TOKENS.
transition, models how to send requests. By
2 sorts OrdPlaceNm OrdTransitionNm MetPlaceNm fi ring this rule a request token is added to the
PlaceName TransitionName MetTransitionNm Marking . interface place pi1 and the same token, but
4 subsorts OrdPlaceNm MetPlaceNm < PlaceName. constrained by a reconfi guration timer τ , is
5 subsorts OrdTransitionNm MetTransitionNm < added to the subsequent state place p12 of
TransitionName.
6 op <_,_>:OrdPlaceNm Tokens->Marking[ctor prec23]. the requester (The timer τ represent the
7 op <_,_>:MetPlaceNm Tokens->Marking[ctor prec23]. maximal waiting duration for a response),
8 op <_,_>:OrdTransitionNm TimeInf->Marking[ctor prec 23]. • Rewriting rule that fi res the receiv-req
9 op <_,_>:MetTransitionNm TimeInf->Marking[ctor prec23]. transition models how to receive requests.
10 op __:Marking Marking->Marking[ctor assoc comm
prec24 id:none].
When applying this rule, a request token is
11 op none:-> Marking [ctor]. consumed from the interface place pi1, the
12 op [_]:Marking-> System [ctor]. initial marking of the place p21 (denoting the
endtm maximum number of possible requests) is
decreased by one, and a token is added to
the subsequent state place p22 of the
Figure 4 Mop-ECATNets Marking as a timed requested service,
module
• The sending reply rewriting rule associated to
tmod ACTIV-TRANS is
transition send-reply is executed when
including MARKING-SPEC . treatment duration of a p22 tokens decreases
op Active : OrdTransitionNm TkId Marking -> Bool . to the value 0, i.e. the request has been
var tk : TkId . var tks : Tokens . var treated, by executing this rule a reply token is
ti : TimeInf .
sent to the interface place pi2,
ops t1 … tn : -> OrdTransitionNm [ctor] .
ops mpt1 …. Mptn : -> MetPlaceNm [ctor] . • A conditional rewriting rule is also associated
eq Active( t1 , tk , < mpt1 , tk tks > M:Marking ) = true . to the transition receiv-reply, it models how to
... ... ... receive a response from a requested Web
eq Active( tn , tk , < mptn , tk tks > M:Marking ) = true.
service. This rule is applied when token
eq Active( t:OrdTransitionNm , tk , M:Marking ) = false
[owise] . treatment duration is lower than
endtm reconfi guration Timer value of the same
token,
Figure 5 Active transitions in a Mop-ECATNet • Adaptation process is handled by the Meta
transition reconf mechanized by a conditional
5.2. Mop-ECATNets and Dynamic Web rewriting rule; this conditional rule is triggered
Service when token reconfi guration Timer expires and
there is no response token in the interface
Dynamic behavior of Mop-ECATNets may be
defi ned independently of the specifi ed system, place pi2. By triggering this rule, we get a new
but in this work we explain its motivation through marking of the higher net component.
Web services components (see Fig. 6). In this Through the proposed defi nitions of this
case, fi ve generic rewriting rules defi ne section, we have achieved a modular and legible
instantaneous behavior of Mop-ECATNets. specifi cation of dynamic Web service
International Conference on Advanced Aspects of Software Engineering
ICAASE, November, 2-4, 2014, Constantine, Algeria. 31
ICAASE'2014 Mop-ECATNets for Dynamic Web Services Formal Modeling
compositions. The expressiveness and
generality of real-time rewrite theories allow us
the declaration of both user defi ned operators
and real-time dynamic behavior. Another
important fact of the rewriting Mop-ECATNet
implementation is that each deduced Maude
module specifi es not just a theory, but a precise
high-level mathematical model. Hence, this
model will serve to the formal checking of any
dynamic web services based system. It is also
worth to mention that the MopECATNet defi nition
presented in this section can serve also in
modeling other systems with temporal
constraints and having dynamic and adaptive
behaviour.
Figure 7 The traveller map web service
6.1. The specification step
We note that our proposed model is generic
enough, it remains valid for any Web service
example. So, in order to formalize the traveller
map composite web service on the basis of Mop-
ECATNets model, we need to declare a new
real-time Maude module extending MARKING-
SPEC and ACTIV-TRANS modules (presented in
section 3) by additional constant operators to
specify: the Traveller map dynamic service
components identifi ers, ordinary places names,
Figure 6 Mop-ECATNets dynamic behavior ordinary transitions name, meta-places name,
meta-transitions name and fi nally tokens
identifi er. Dynamic behavior of our case study is
6. CASE STUDY automated by a set of rewriting rules and their
effects on the corresponding Mop-ECATNet
In order to illustrate our proposed model, we elements.
consider in this section the traveller map web
service as case study (Fig. 7). This composite 6.2. Analysis of the traveller map service
service is initially composed of two services: a
mobile map requester and a primary map In order to check our traveller map dynamic
provider service, and can be adapted at service we defi ne the module MODEL-CHECK-
reconfi guration time by integrating a secondary TRAV-MAP-BEHAV (Fig. 8). In this module, we
map service provider in case of failure. import the traveler map dynamic behavior
module TRAV-MAP-BEHAV (not presented here
due to lack of space), as well as the prede fi ned
module TIMED-MODEL-CHECKER. Then, we
defi ne some useful atomic parameterized
propositions (equations of the module in Fig. 8):
International Conference on Advanced Aspects of Software Engineering
ICAASE, November, 2-4, 2014, Constantine, Algeria. 32
ICAASE'2014 Mop-ECATNets for Dynamic Web Services Formal Modeling
1. The atomic proposition delay-elapsed is used In this section, we have illustrated by using
to defi ne tokens reconfi guration timer the traveller map dynamic service how to use our
expiration; model. More precisely, we have showed how a
Mop-ECATNet based specifi cation may be
2. reconf-start which checks triggering of formally analyzed against dynamic system
adaptation process for a request; requirements. Obtained results confi rm
3. success that confi rms accomplishment of a usefulness of this model, it takes into account
request. many aspects of dynamic systems. In fact, Mop-
ECATNets have the ability to model systems
For this paper, we restrict our self to verify having concurrent, timed, dynamic and
three compound properties (Fig. 9). The fi rst reconfi gurable behavior also dataflow aspect is
timed command checks whether the delay considered. Rewriting logic is unifying logical and
expiration in time less or equal to four time units semantic framework; this implies that Mop-
is possible. The second timed command checks ECATNets can be linked easily with other
if delay expiration for the request appears, it will formalisms.
be always followed by the triggering of
adaptation process. Finally, we check absence of
successful treatment in time less or equal to four 7. CONCLUSION
time units. The result of these commands is
showed in fig. 9. In this work, we have introduced Mop-
ECATNets as a new Petri net based model,
(tmod MODEL-CHECK-TRAV-MAP-BEHAV is devoted to raise reliability of dynamic Web
including TIMED-MODEL-CHECKER . services design and re alization. The proposed
protecting TRAV-MAP-BEHAV.
vars tks tks' tks'' : Tokens . var tk : TkId .
model inherits a set of useful constructs from
var SYSTEM : System . var REST : Marking . other Petri net models and allows developer to
op delay-elapsed : TkId -> Prop [ctor] . reason correctly about dynamic features at
op reconf-start : TkId -> Prop [ctor] . design time thanks to its integration in timed
op success : TkId -> Prop [ctor] . rewriting logic. We have shown how this logic
eq {[ < p2, tk [ 0 ] tks > REST ]} |= delay-elapsed(tk) = true . provides a flexible conceptual framework, where
eq {[ < mpt1', tk tks > < mpt2',tk tks' > < mtr, tk tks'' > REST ]} |= Mop-ECATNets can be naturally seen as a timed
reconf-start(tk) = true . rewrite theory. A nice consequence of this
eq {[ < p3 , tk tks' > REST ]} |= success(tk) = true . endtm)
axiomatization is that relationship between the
two defi ned Petri net levels, Metalevel for
reconfi guration process and basic one for service
Figure 8 The module MODEL-CHECK-TRAV-MAP- model, was formally established. In addition
BEHAV dynamic properties of a Mop-ECATNet were
Model check{TravMS} |=t <> delay-elapsed(tk:TkId) in
checked and deduced, in particular traveller map
MODEL-CHECK-DYN-TRAVLER-SERV dynamic service case study has been used to
in time <= 4 with mode default time increase 1 illustrate our model and check some useful
Result[ModelCheckResult]: properties.
counterexample({{[< mpt1,tk1 tk2 tk3 > ..in time 0,'t1}{{[<…in
time 0,'t3}{{[ in time 0, In the proposed model, services are adapted
unlabeled}{{[… in time 0,'t1… in time 0,'t3}{{[… in time by substitution caused by the time expiration. As
0,unlabeled}{{[< ….]} in time 4,'tick}) future works, we will focus on modeling other
=============== adaption triggering events like users’ profi le
Model check{TravMS} |=t[](delay-elapsed(tk:TkId)=> <> changes and appearance of more adjusted
reconf-start(tk)) in services.
MODEL-CHECK-DYN-TRAVLER-SERV in time <= 6 with mode
default time increase 1
Result Bool : true 8. References
=================
Model check{TravMS} |=t[]~ success(tk:TkId)in MODEL-
[1] O. Ezenwoye, S. Busi, and S. M. Sadjadi,
CHECK-DYN-TRAVLER-SERV “ Dynamically reconfigurable data-intensive
in time <= 4 with mode default time increase 1 service composition,” in WEBIST (1), pp.
Result[ModelCheckResult]: 125– 130, 2010.
counterexample({{[< mpt1,tk1 > < mpt1',(none).Tokens > <
[2] D.H. Xu, Y. Qi, D. Hou, Y. Chen, and L. Liu,
mpt2,tk1 > < mpt2',( “ A formal model for dynamic web services
none).Tokens > … < tr,INF >]} in time 4, 'tick})
composition mas-based and simple security
analysis using spi calculus,” in Proceedings
Figure 9 Examples of the traveller map dynamic of the Third International Conference on
service properties analysis Next Generation Web Services Practices,
International Conference on Advanced Aspects of Software Engineering
ICAASE, November, 2-4, 2014, Constantine, Algeria. 33
ICAASE'2014 Mop-ECATNets for Dynamic Web Services Formal Modeling
NWESP ’07, (Washington, DC, USA), pp. Computing, SYNASC ’06, (Washington, DC,
69– 72, IEEE Computer Society, 2007 USA), pp. 389– 398, IEEE Computer
[3] F. Latreche, H. Sebih, and F. Belala, Society, 2006.
“ Analyzing web service interaction using [18] N. Boudiaf and A. Chaoui, “ Double reduction
open ecatnets,” in ACIT2011 International of ada-ecatnet representation using rewriting
Conference on Information and Technology, logic,” Enformatika Journal (Transactions on
2011. Engineering, Computing and Technology),
[4] C. A. Petri, Kommunikation mit Automaten. vol. 15, pp. 278– 284, October 2006.
PhD thesis, Darmstadt University of
Technology,Germany, 1962.
[5] V. Savolainen and V. Terziyan,
“ Metapetrinets for controlling complex and
dynamic processes,” 1999.
[6] J. Meseguer, “ Conditional rewriting logic as
a unified model of concurrency,” Theor.
Comput.Sci., vol. 96, pp. 73– 155, Apr. 1992.
[7] P. C. Olveczky, Real-Time Maude 2.3
Manual, 2007.
http://www.ifi.uio.no//RealTimeMaude/.
[8] R.Hamadi, and B. Benatallah, “ A Petri Net-
based Model for Web Service Composition”.
In: ADC, 17, pp. 191-200, 2003.
[9] N. Lohmann, P. Massuthe, C. Stahl and D.
Weinberg, “ Analyzing Interacting WS-BPEL
Processes”, in Proc. Int. Conf. Business
Process Management, pp. 17– 32, 2006.
[10] W. M. van der Aalst, A. J. Mooil, C. Stahl
and K. Wolf, “ Service Interaction: Patterns,
Formalization, and Analysis,” In: Formal
Methods for Web Services - 9th International
School on Formal Methods for the Design of
Computer, Communication and Software
Systems: Web Services, LNCS, vol. 5569,
2009.
[11] T. Lu and J. Bao, “ A systematic approach to
context aware service design,” JCP, vol. 7,
no. 1,pp. 207– 217, 2012.
[12] D. Zhovtobryukh, Context-aware Web
Service Composition. Jyvaskyla studies in
computing,University of Jyvaskyla, 2006.
[13] . C. Olveczky and J. Meseguer, “ Semantics
and pragmatics of real-time maude,” Higher
Order Symbol. Comput., vol. 20, pp. 161–
196, June 2007.
[14] K. Bae and P. C. Olveczky, “ Extending the
real-time maude semantics of ptolemy to
hierarchical de models,” in RTRTS (P. C.
Ö lveczky, ed.), vol. 36 of EPTCS, pp. 46–
66, 2010.
[15] M. Bettaz and M. Maouche, “ How to specify
non-determinism and true concurrency with
algebraic term nets,” in Selected papers
from the 8th Workshop on Specification of
Abstract Data Types Joint with the 3rd
COMPASS Workshop on Recent Trends in
Data Type Specification, (London, UK, UK),
pp. 164– 180, Springer-Verlag, 1993.
[16] M. Bettaz, M. Maouche, and K. Barkaoui,
“ Formal specification of communication
protocols with object-based ecatnets.,” in
EUROMICRO, pp. 492– , IEEE Computer
Society, 1996.
[17] A. Hicheur, K. Barkaoui, and N. Boudiaf,
“ Modeling workflows with recursive
ecatnets,” in Proceedings of the Eighth
International Symposium on Symbolic and
Numeric Algorithms for Scientific
International Conference on Advanced Aspects of Software Engineering
ICAASE, November, 2-4, 2014, Constantine, Algeria. 34