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