- 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.
Service Oriented Architecture (SOA) is a development model aiming at raising integration and interoperability of software components. In SOA services are units of work, they are selfdescribing modular applications that can be published, localized and invoked across the web thanks to a set of XML standards. In most cases elementary services cannot carry out required functionalities. Thus, we need invoking several Web services and then composing them in order to reach new personalized, rich and more interesting functionalities.
Several efforts on web service modeling and analysis have already been done by researchers and industrial practitioners. But, mostly these works pay less attention to dynamic features. Also, current Web service standards and languages provide limited constructs for specifying exceptional behavior [1] [2], and they are semi-formal requiring translation to generate formal models that admit checking.
In this work, we propose using
MopECATNets (Meta Open Extended Concurrent
Algebraic Term Nets) to enhance design and
analysis of dynamic Web services.
MopECATNets are an extended version of
OpenECATNets [
Since their introduction, by Carl Adam Petri
[
Rewriting logic is a general framework, in
which not just applications, but entire formalisms
and computation models can be naturally
expressed. This logic allows correct reasoning on
concurrent systems behavior. Several practical
languages were invented on the basis of
rewriting logic, the most known is Maude (SRI
laboratory, United States)[
The remainder of this paper is organized as follows. In section 2, we give an overview of related works. Sections 3 and 4 introduce the real-time rewriting logic and Open-ECATNets model. In Section 5, we deal with the MopECATNets model for dynamic Web services. We identify its integration in real-time rewriting logic semantic framework, so both structural and behavior aspects are considered. In section 6, we illustrate our formalization approach by means of a realistic case study, the traveller map dynamic service. We also show how some relevant properties are formally checked. The paper is outlined by some concluding remarks and perspectives.
Several attempts [08] [09] [
Authors of [
In a similar work [
Our approach for specifying and analyzing dynamic Web services is quite different, since it uses useful features of many Petri nets models and it’s based on a unique semantic framework: real-time rewriting logic. Mop-ECATNets are also executable; they are able to reconfi gure dynamically their structure. Thus, services failures are conditions that trigger adaptation actions. Besides, our developed model allows formal checking of some inherent properties related to dynamic Web services thanks to the Real Time Maude model checker tool.
The objective of this section is to present
elementary concepts of real-time rewriting logic
for more details, reader can refer to [
Since its introduction, rewriting logic has
attracted the interest of both theorists and
practitioners. Its experimentation through many
applications has conducted to propose some
extensions of this logic. The most signifi cant one
is the real-time rewriting logic allowing
specifi cation of real-time systems. Basic
specifi cation elements of real-time rewriting logic
are real-time rewrite theories [
Real-Time Maude is an extension of Maude.
It emphasizes ease and generality of
specifi cation, including support for distributed
real-time object based systems. Also, it provides
a large range of simulation and analysis
techniques. This tool complements other
realtime analysis tools not only by the full generality
of the specifi cation language and the range of
analysis techniques, but also by its simplicity and
clarity. Real-time and hybrid systems are
represented as real-time rewrite theories, where
equations are used to specify data types and
rewrite rules to mechanize dynamic and real-time
behavior.
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
model checking to explore many concurrent
behaviors of a system [
In addition to the use of rewriting logic in
specifi cation of concurrent and distributed
system semantics, it is also a promising logical
framework in which many logics and concurrency
models as ECATNets [
Definition 1. An ECATNet (see Fig. 1) is a high level Petri net having the structure (P, T, sort, IC, DT, CT, TC), where: • P and T are respectively fi nite sets of places and transitions (with P∩ T=ø ); • sort: P→ S is a function that associates to each place an algebraic sort s of Σ ; • IC (Input Condition):P×T→ MTΣ /EUA(X), is a function that specifi es partial conditions on input place markings; • DT (Destroyed Tokens): P× T → MTΣ /EUA(X), is another function that associates to each input arc (p×t) of transition t, a multi-set of algebraic terms to be consumed from input place; • CT (Created Tokens): P× T→ MTΣ /EUA(X) associates to each output place of P, a multiset of algebraic terms which may be added when a transition is fi red; • TC (Transition Condition) is an additional condition, when it is omitted, the default value is the term true.
A distinctive characteristic of ECATNets is
their strength in modeling synchronization
constraints and complex system data structures.
They have been largely applied in modeling and
checking various kinds of systems [
In an Open-ECATNet, the set of interface places (IO) are designed to defi ne external interaction and the set of state places (ST) to model services states.
Open-ECATNet (or ECATNet) behavior is defi ned by way of concurrent computations in rewriting logic. Each transition is materialized by a local rewriting rule of a given rewrite theory defi ning the distributed structure of ECATNet states.
Because of their size and complexity, distributed and dynamic systems, as Web services, may not be easily modeled. They require using more tailored formalisms. Dynamic web services are highly affected by time. A rigorous approach to tackle failures is to fix a maximal waiting time before launching adaptation process. The objective of this section is to present the Mop-ECATNets model, designated to better specify and analyze dynamic Web services.
To allow a flexible modeling of complex
dynamic Web service process, we enhance
Open-ECATNets with the Meta Petri nets
features [
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 elapsed time after the sending request action is equal to a fi xed maximum delay). Formally, the Mop-ECATNet defi nition is given by:
Defi nition 3. A Mop-ECATNet ME =< E, O, Q, λ> is a two levels Meta transitional net having as higher level net the marked ECATNet E and as lower level the Open-ECATNet O. Q is the incidence function mapping meta places of E to transitions of O and λ: ST → N is a function that maps each state place (belonging to ST) to its reconfi guration timer.
Let’s recall that: E = (P’, T’, sort’, IC’, DT’, CT’, TC’) and O = {(IO∪ST, T, sort, IC, DT, CT, TC), Mi, Mf}. In Fig. 2, we give a Mop-ECATNet, where places mpt and mpt’ are the meta places relative to transitions t and t’ of the lower OpenECATNet. The Mop-ECATNet of this fi gure can also be defi ned by the following sets: P’= {mpt, mpt’ }, T’= {mt}, Q = {(mpt, t), (mpt’, t’)}, IO = {pi, pi’ }, ST = {p1, p2, p3},Mi = {(1, 0, 0)} , Mf = {(0, 1, 0), (0, 0, 1)} and λ= {(p3, 3)}.
Our formalization of a Mop-ECATNet is based on the following idea: a net marking is considered as a multi-set of algebraic terms modeling places and its transitions as a multi-set of rewriting rules. In order to mechanize instantaneous fi ring of transitions, we add a timer for each transition t belonging to T U T’. This timer has either the value 0 to denote forced to fi re transitions, or the value INF (infi nity) for non fi rable transitions.
Thus, Mop-ECATNets are defi ned in terms of timed rewrite theories. Three timed Maude modules TOKENS, MARKING-SPEC and ACTIV-TRANS (Fig. 3 to Fig. 5) are designed to implement our Mop-ECATNets model. The Figure 3 shows a slightly modifi ed version of the timed Maude module TOKENS that represent tokens abstract data types. In this module, we fi rstly import the predefi ned module NAT-TIMEDOMAIN-WITH-INF defi ning the time domain to be the natural numbers with the infi nity value. Then, we declare a set of sort and subsort relations useful to describe statically MopECATNet tokens (a multi-set of algebraic terms having the form tkid, tkid[t], where tkid is the token identifi er and t represent the container place reconfi guration timer).
Mop-ECATNets Marking is then formalized by the timed module MARKING-SPEC (Fig. 4). According to our formalization, markings are viewed as multi-sets of ordinary places, Meta places, ordinary transitions and Meta transitions (operations declared in lines 6, 7, 8 and 9 of Fig. 4). Let’s note that in the case of transition, its algebraic term must have the form < t, r >, where t is the name of transition and r is its timer value.
The third timed module ACTIV-TRANS (Fig. 5) defi nes, thanks to a set of equations, in which case a given transition is active regarding a particular token (the send or receive action is enabled for a particular exchanged message).
For Mop-ECATNets model, it is worth noting that formalized services may be extended to model new Web service composition concepts, and will make easy their interconnection with services of other applications in the context of heterogeneous systems. Also, time which is currently an important aspect of Web services, is straightforwardly modeled thanks to real-time extension of Maude. Furthermore, checking Mop-ECATNets specifi cations is now possible thanks to the Real Time Maude analysis tools. tmod TOKENS is including NAT-TIME-DOMAIN-WITH-INF. sorts Token Token. subsort Token Nat < Tokens. subsort TkId < Token. op _`[_`] : TkId Time -> Token [ctor prec 21]. op __ : Tokens Tokens -> Tokens [ctor assoc comm prec 22 id: none ]. op none : -> Tokens [ctor]. endtm
Dynamic behavior of Mop-ECATNets may be defi ned independently of the specifi ed system, but in this work we explain its motivation through Web services components (see Fig. 6). In this case, fi ve generic rewriting rules defi ne instantaneous behavior of Mop-ECATNets. These rules model fi ring of Mop-ECATNets transitions when their timers have the value 0. As results of fi ring, some tokens are removed from defi nite places and added to other places, transition timers are turned off ( fi xed to the infi nity value), and the function recomputeTimers is applied to the entire resulting state to recompute all transition timer values. Particularly, this function tests if a transition is enabled, then its timer is reinitialized to the value 0, otherwise the timer is left unchanged. More precisely, for each transition of a generic Mop-ECATNet (see Fig. 6) we associate a rewriting rule having the following interpretation: • The rewriting rule associated to send-req transition, models how to send requests. By fi ring this rule a request token is added to the interface place pi1 and the same token, but constrained by a reconfi guration timer τ , is added to the subsequent state place p12 of the requester (The timer τ represent the maximal waiting duration for a response), • Rewriting rule that fi res the receiv-req transition models how to receive requests. When applying this rule, a request token is consumed from the interface place pi1, the initial marking of the place p21 (denoting the maximum number of possible requests) is decreased by one, and a token is added to the subsequent state place p22 of the requested service, • The sending reply rewriting rule associated to transition send-reply is executed when treatment duration of a p22 tokens decreases to the value 0, i.e. the request has been treated, by executing this rule a reply token is sent to the interface place pi2, • A conditional rewriting rule is also associated to the transition receiv-reply, it models how to receive a response from a requested Web service. This rule is applied when token treatment duration is lower than reconfi guration Timer value of the same token, • Adaptation process is handled by the Meta transition reconf mechanized by a conditional rewriting rule; this conditional rule is triggered when token reconfi guration Timer expires and there is no response token in the interface place pi2. By triggering this rule, we get a new marking of the higher net component.
Through the proposed defi nitions of this section, we have achieved a modular and legible specifi cation of dynamic Web service 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.
In order to illustrate our proposed model, we consider in this section the traveller map web service as case study (Fig. 7). This composite service is initially composed of two services: a mobile map requester and a primary map provider service, and can be adapted at reconfi guration time by integrating a secondary map service provider in case of failure.
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 MopECATNets model, we need to declare a new real-time Maude module extending MARKINGSPEC 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, ordinary transitions name, meta-places name, meta-transitions name and fi nally tokens identifi er. Dynamic behavior of our case study is automated by a set of rewriting rules and their effects on the corresponding Mop-ECATNet elements.
In order to check our traveller map dynamic service we defi ne the module MODEL-CHECKTRAV-MAP-BEHAV (Fig. 8). In this module, we import the traveler map dynamic behavior module TRAV-MAP-BEHAV (not presented here due to lack of space), as well as the predefi ned module TIMED-MODEL-CHECKER. Then, we defi ne some useful atomic parameterized propositions (equations of the module in Fig. 8): 1. The atomic proposition delay-elapsed is used to defi ne tokens reconfi guration timer expiration; 2. reconf-start which checks triggering of adaptation process for a request; 3. success that confi rms accomplishment of a request.
For this paper, we restrict our self to verify three compound properties (Fig. 9). The fi rst timed command checks whether the delay expiration in time less or equal to four time units is possible. The second timed command checks if delay expiration for the request appears, it will be always followed by the triggering of adaptation process. Finally, we check absence of successful treatment in time less or equal to four time units. The result of these commands is showed in fig. 9.
(tmod MODEL-CHECK-TRAV-MAP-BEHAV is including TIMED-MODEL-CHECKER . protecting TRAV-MAP-BEHAV. vars tks tks' tks'' : Tokens . var tk : TkId . var SYSTEM : System . var REST : Marking . op delay-elapsed : TkId -> Prop [ctor] . op reconf-start : TkId -> Prop [ctor] . op success : TkId -> Prop [ctor] . eq {[ < p2, tk [ 0 ] tks > REST ]} |= delay-elapsed(tk) = true . eq {[ < mpt1', tk tks > < mpt2',tk tks' > < mtr, tk tks'' > REST ]} |= reconf-start(tk) = true . eq {[ < p3 , tk tks' > REST ]} |= success(tk) = true . endtm) Model check{TravMS} |=t <> delay-elapsed(tk:TkId) in MODEL-CHECK-DYN-TRAVLER-SERV in time <= 4 with mode default time increase 1 Result[ModelCheckResult]: counterexample({{[< mpt1,tk1 tk2 tk3 > ..in time 0,'t1}{{[<…in time 0,'t3}{{[ in time 0, unlabeled}{{[… in time 0,'t1… in time 0,'t3}{{[… in time 0,unlabeled}{{[< ….]} in time 4,'tick}) =============== Model check{TravMS} |=t[](delay-elapsed(tk:TkId)=> <> reconf-start(tk)) in
MODEL-CHECK-DYN-TRAVLER-SERV in time <= 6 with mode default time increase 1 Result Bool : true ================= Model check{TravMS} |=t[]~ success(tk:TkId)in MODELCHECK-DYN-TRAVLER-SERV in time <= 4 with mode default time increase 1 Result[ModelCheckResult]: counterexample({{[< mpt1,tk1 > < mpt1',(none).Tokens > < mpt2,tk1 > < mpt2',( none).Tokens > … < tr,INF >]} in time 4, 'tick}) Figure 9 Examples of the traveller map dynamic service properties analysis
In this section, we have illustrated by using the traveller map dynamic service how to use our model. More precisely, we have showed how a Mop-ECATNet based specifi cation may be formally analyzed against dynamic system requirements. Obtained results confi rm usefulness of this model, it takes into account many aspects of dynamic systems. In fact, MopECATNets have the ability to model systems having concurrent, timed, dynamic and reconfi gurable behavior also dataflow aspect is considered. Rewriting logic is unifying logical and semantic framework; this implies that MopECATNets can be linked easily with other formalisms.
In this work, we have introduced MopECATNets as a new Petri net based model, devoted to raise reliability of dynamic Web services design and re alization. The proposed model inherits a set of useful constructs from other Petri net models and allows developer to reason correctly about dynamic features at design time thanks to its integration in timed rewriting logic. We have shown how this logic provides a flexible conceptual framework, where Mop-ECATNets can be naturally seen as a timed rewrite theory. A nice consequence of this axiomatization is that relationship between the two defi ned Petri net levels, Metalevel for reconfi guration process and basic one for service model, was formally established. In addition dynamic properties of a Mop-ECATNet were checked and deduced, in particular traveller map dynamic service case study has been used to illustrate our model and check some useful properties.
In the proposed model, services are adapted by substitution caused by the time expiration. As future works, we will focus on modeling other adaption triggering events like users’ profi le changes and appearance of more adjusted services. 8. References [1] O. Ezenwoye, S. Busi, and S. M. Sadjadi, “ Dynamically reconfigurable data-intensive service composition,” in WEBIST (1), pp. 125– 130, 2010. [2] D.H. Xu, Y. Qi, D. Hou, Y. Chen, and L. Liu, “ A formal model for dynamic web services composition mas-based and simple security analysis using spi calculus,” in Proceedings of the Third International Conference on Next Generation Web Services Practices, NWESP ’07, (Washington, DC, USA), pp. 69– 72, IEEE Computer Society, 2007