Access the full text.
Sign up today, get DeepDyve free for 14 days.
Loading next page...
/lp/taylor-francis/using-unified-modelling-language-to-model-the-publish-subscribe-9gE59kk5HR
References
References for this paper are not available at this time. We will be adding them shortly, thank you for your patience.
- Publisher
- Taylor & Francis
- Copyright
- © 2017 The Author(s). Published by Informa UK Limited, trading as Taylor & Francis Group.
- ISSN
- 1744-5051
- eISSN
- 1387-3954
- DOI
- 10.1080/13873954.2016.1277360
- Publisher site
- See Article on Publisher Site
Abstract
MATHEMATICAL AND COMPUTER MODELLING OF DYNAMICAL SYSTEMS, 2017 VOL. 23, NO. 6, 570–594 https://doi.org/10.1080/13873954.2016.1277360 Using unified modelling language to model the publish/ subscribe paradigm in the context of timed Web services with distributed resources Valentín Valero and María-Emilia Cambronero Department of Computer Science, University of Castilla-La Mancha, Albacete, Spain ABSTRACT ARTICLE HISTORY In this paper, we present a unified modelling language (UML) framework Received 2 March 2016 to model timed Web services with distributed resources. We provide a Accepted 24 December 2016 graphical model of timed Web services that integrates the publish/sub- KEYWORDS scribe paradigm in the context of distributed resources, with the goal UML 2.4.1; process algebras; that users have a formal framework to design this kind of systems. A WSRF; WS-BaseNotification; formalization is then provided by using UML sequence diagrams with distributed resources; Combined Fragments (CFs) to represent the interactions between the distributed systems roles involved and Web Services Resource Framework as a standard for the management of distributed resources. The formalization is based on a two-level process algebra. At the top level we have the CF description, and at the bottom the interactions inside them. An operational seman- tics is then defined for this model, and two case studies are presented to illustrate the applicability of this formalism. 1. Introduction The classical Web service definition [1] does not consider the notion of state, but interfaces frequently provide the user with the ability to access and manipulate states, that is, data values that persist and evolve as a result of Web service interactions. It is therefore desirable to define Web service conventions to enable the discovery of, introspection on, and interaction with stateful distributed resources in standard and interoperable ways. This is the primary goal of this paper, and to do so we have used unified modelling language (UML) 2.4.1 sequence diagrams (SDs) extended with Combined Fragments (CFs) [2] for the modelling of workflows of interactions among the participants and resources involved. CFs allow us to define control structures for interaction fragments, which delimit interactions blocks of the involved participants. Using them we have a graphical and structured representation of the message exchanges among all the participants in a Web service composition. We focus our attention to timed Web services managing a collection of distributed resources, so we integrate the publish/subscribe paradigm and the OASIS Web Services Resource Framework (WSRF) standard [3] in this framework. WSRF is the de facto OASIS standard for modelling and accessing stateful resources using Web services, so it provides us with standardized operations for the management of resources. All of these technologies allow us to improve the communication between different services, facilitating the interoperability among them. The modelling of this kind of systems is a primary task to under- stand how they work and analyse their behaviour, so a formal framework is therefore defined to model these systems, which is based on UML 2.4.1 [2], but including the main aspects of WSRF. CONTACT María-Emilia Cambronero MEmilia.Cambronero@uclm.es © 2017 The Author(s). Published by Informa UK Limited, trading as Taylor & Francis Group. This is an Open Access article distributed under the terms of the Creative Commons Attribution-NonCommercial-NoDerivatives License (http:// creativecommons.org/licenses/by-nc-nd/4.0/), which permits non-commercial re-use, distribution, and reproduction in any medium, provided the original work is properly cited, and is not altered, transformed, or built upon in any way. MATHEMATICAL AND COMPUTER MODELLING OF DYNAMICAL SYSTEMS 571 This formalism is based on a two-level timed process algebra, in which we define the CFs behaviour at the top level, and the interactions that take place inside these CFs at the bottom level. A preliminary (untimed) version of this work was published in [4], where a smaller set of UML 2.0 constructions was considered and time aspects were not included in the model. We now use UML 2.4.1 SDs with the CFs extension [2] to describe the flows of collaborations among the participants and resources involved in a Web service composition, in terms of the message exchanges among all of them. Regarding the time model, we will consider a discrete model with a global clock which progresses monotonically in the forward direction. The alternative to discrete time models are continuous time models, which are normally preferred, as they use a real timescale, and thus, in principle, the execution of actions is not restricted to discrete points in time. However, as Baeten and Middelburg mention in [5], measuring time on a discrete timescale does not mean exactly this, but to divide time into slices and to time actions with respect to the time slices in which they are carried out. Actually, computers measure time by means of discrete clocks, and if they are used to control a physical system, the state of the physical system is sampled and adjusted to discrete points in time. Furthermore, we have local variables (for the participants involved) and distributed resources, whose values or properties move within specific domains. Variable values can be assigned, read, or checked in guards, whereas resources are assumed to have a lifetime and a single property, and are manipulated by the WSRF operators. As we mentioned above, at the top level we introduce the CFs behaviour, that is, a description of the CF structure for the system considered, using the following basic control structures: parallel (par), strict sequencing (strict), guarded choice (alt), and iteration (loop). These are the most relevant operators, capturing the main control structures usually considered in the scope of workflows, and rich enough to describe the general workflows of interactions among the parti- cipants and the resources they use. On the other hand, at the bottom level, we describe the basic interactions inside each CF, taking the following model of basic interactions: as single local actions we have a no-action (nil)of a participant, the assignment of variables (assign), delays (wait), and behaviour executions, denoted by letters a, b, .... The latter denote actions performed by a single participant, which can have an execution occurrence specification associated, indicating a restriction for their starting times. A message exchange is represented by the operators send and recv, executed by the participants involved in the CF. There is also the possibility to send or receive messages outside a CF, by using gates, and we have the operators gsend and grecv for this purpose. We also have the operations related to the management of distributed resources, according to the WSRF [3] and Web Services Notification (WSN) [6] standards. Furthermore, we need operations for the publish- ing and discovery of resources, which are not included in the WSRF standard. Actually, it is left to the implementation to determine the way in which resources are created, published and dis- covered, so we have decided to include specific operations for this purpose. The rest of the paper is organized as follows. The related work is presented in Section 2, and the background described in Section 3, where we summarize the main aspects of UML 2.4.1 SDs (extended with CFs), as well as the main elements of WSRF/WSN that we will consider through- out the paper. The UML+WSRFN model is formally introduced in Section 4, and the two-level operational semantics is defined in Section 5. Two case studies to illustrate this formalism are presented in Section 6, and Section 7 finishes the paper by providing some conclusions and possible lines of future work. 2. Related work Formal methods have been extensively used for the description of distributed systems. Bravetti and Zavattaro [7] discuss the main aspects of service-oriented computing and their relation with 572 V. VALERO AND M.-E. CAMBRONERO process algebra operators. They define a (timed) process algebra based on the following aspects of service-oriented computing: loose coupling, communication latency, and open-endness. Formal models are also extensively applied to UML. R. Mirandola and V. Cortellessa [8] make use of UML diagrams, in particular use case diagrams, SDs, and deployment diagrams, in order to obtain a performance model of the system based on a queueing network, which can therefore be helpful as a support for early design decisions. Tribastone and Gilmore [9] have defined a translation of UML SDs annotated with stochastic information into the stochastic process algebra PEPA [10]in order to carry out quantitative evaluation. Bran Selic [11] presents a generic framework for modelling resources with UML, focusing on the notion of abstract resources, which define the common characteristics of resources regardless of their specific manifestation. Resources are modelled in that work as servers with services, characterized by both their functional and non-functional aspects, such as response time and availability, focusing on Quality of Service analysis. Thus, Selic’s work does not introduce a formal language to describe resources, or the publish/subscribe pattern. The publish/subscribe paradigm has received considerable attention in the last few years. A survey on this subject was carried out by Lin and Plade [12], and formalizations of this paradigm can be found in [13,14]. From these works it becomes obvious that the way in which the publish/ subscribe systems are modelled varies considerably depending on the specific model’s goals. In our case, we will only need a mechanism to publish distributed resources identified by a textual name, and a mechanism to allow clients to discover these resources, by using these names. We omit a discussion about rules or policies to resolve the discovery problem, since for our purposes any resource whose identifier matches the given name will be valid. Continuing with UML formalizations, Hlaoui et al. [15] use a domain specific language (DSL) based on UML activity diagrams to specify and systematically compose workflow models from grid services. They present a formal framework to transform UML activity diagrams specifying workflows composed from grid services to the WS-BPEL language describing Web services workflows. However, distributed resources are not considered in that work, and neither is the publish/subscribe pattern. Pllana et al. [16] have developed a graphical editor Teuta for the specification of scientific grid workflows. They have defined a DSL for grid workflows that is based on activity diagrams of UML 2.0, in order to graphically compose the workflows by combining some predefined elements of the language. A transformation of UML 2 SDs into State Machines by using graph transformation techniques has been defined by Grønmo and Møller-Pedersen [17], by taking the parallel, choice, loop, and neg CFs, but again time and resources are not considered in this approach. There is also a work by Lund and Stølen [18], in which an operational semantics for SDs of UML 2.0 is defined, with operators to capture strict sequential composition, parallel and two choices (potential and mandatory), but basic interactions are reduced to message exchanges inside a single frame and neither time restrictions nor distributed resources are considered. Thus, to our knowledge there is no work that combines the main features of UML 2.4.1 SDs with the WSRF standard in a two-level algebraic language for the description of distributed resources. In a preliminary work [4] we used a smaller set of UML 2.0 constructions, and time aspects were not included. In [19] we used the RT-UML profile [20] for UML 2.0 and we defined a corresponding process algebra capturing the main aspects related to SDs extended with CFs in order to obtain a translation into a network of timed automata, so the modelled system can be simulated and analysed by using one of the existing tools supporting timed automata, such as UPPAAL [21]. In this work resources were not considered, so the current work extends this previous article by introducing a WSRF-compliant model of distributed resource management, including the publish/subscribe paradigm, and some additional CFs and basic interactions in the model. In [22] we also considered UML 2.0 SDs with CFs to obtain a translation into Web Services Choreography Description Language [23], and a tool was developed to support this MATHEMATICAL AND COMPUTER MODELLING OF DYNAMICAL SYSTEMS 573 process, namely Web Services Translation Tool [24]. In this same line of work Mateo et al. [25] have defined a process algebra that combines orchestrations written in WS-BPEL [26] with distributed resources described by WSRF. 3. Background In this section we describe the main aspects of UML SDs extended with CFs [2], and the WSRF standard [3,27], and specifically, those that will be used throughout the paper. 3.1. UML sequence diagrams and Combined Fragments A SD of UML 2.4.1 [2] depicts the message exchanges that occur in a particular scenario of a system. They show the interactions between the objects or participants in this scenario arranged in a time sequence. The primary goal of SDs is therefore to show the sequences of interactions that take place among the participants in a specific scenario, and not the internal actions these objects perform, which are usually omitted. However, in some cases it can be of interest to show some relevant internal actions, such as the assignment of a variable or the specific response to a received message. These internal actions (ExecutionSpecifications in UML terminology) are then pictured by using boxes enclosing the actions which are linked with the participant lifeline point at which they are performed, and may have a starting time and duration associated with them. It is usual practice to write the participant or object that sends the first message or performs the first action on the left-hand side of the diagram. Subsequent messages and actions are always pictured slightly lower than the previous ones. Messages or method invocations are drawn by using arrows with solid arrowheads, placing the message name or method invocation name with its parameters above the arrowed line. We do not draw return messages, but some method invocations may return some results on some parameters. CFs allow us to extend SDs in a hierarchical way, in order to include some control structures, such as parallel, guarded choice and loops. CFs are therefore defined as units of behaviour, and contain, among other things, the set of objects that are in relation, and the message exchanges between these objects. These are drawn as labelled boxes enclosing these message exchanges and other actions of interest, where the CF operator label is placed in the top-left corner, in a dog-eared rectangle (namebox). These are the CFs we use (Figure 1 depicts some of them): alt: This allows us to specify a guarded choice between two or more operands. It is even possible to include an else part, to indicate the message exchanges that occur when no guard has been evaluated as true. When two or more guard conditions attached to different alternative operands become true, only one of these alternatives is finally performed, but no indication is made in the standard about how to choose it, so we consider this choice as nondeterministic. Notice that the guard condition is placed in the top left part of each argument section, over the corresponding lifeline, which is usually that of the participant that owns the variable or variables checked in the guard condition, because the first message will normally be sent by this participant once it has checked that the condition holds. opt: This allows us to describe the message exchanges that only occur when a certain condition holds, otherwise no action is performed within this CF. When the guard is not present, this CF is considered as optional, so the indicated message exchanges may occur or not. Option CFs are therefore a shorthand of alt-CFs with a single argument, without an else part. When the guard is omitted, an opt-CF is also equivalent to an alt-CF, by using two arguments both with guard true, one with the opt-CF behaviour, and the other empty (Figure 2). 574 V. VALERO AND M.-E. CAMBRONERO Role Role Role Role Role Role 1 i n 1 i n alt opt [guard1] msg [guard] msg msg msg [guard2] msg msg msg [else] msg msg Role Role Role Role Role Role 1 i n 1 i n loop par [guard] msg msg msg msg msg msg msg Figure 1. Some UML 2.4.1 Combined Fragments. Role Role Role Role Role Role 1 i n 1 i n opt alt msg [true] msg msg msg msg [true] msg Figure 2. Modelling an opt-CF without guard with an alt-CF. loop: This allows us to describe a repetitive behaviour, depending on the condition below the loop label. Thus, the message exchanges inside the frame are performed as long as the condition remains true. par: This represents the simultaneous execution of the operands, as a merging of their behaviours. The basic interactions send and recv are only allowed to exchange messages between the participants inside the CF involved. For external messages that must be sent or received outside the CF, we have the operations gsend and grecv, in which a gate must be specified as a connection point for message transmission. Gates are identified by a name, and establish a link between the sender and receiver of a specific message. strict: This represents the classical strict sequence of behaviours, all actions of the first operand must have finished before starting the actions of the second operand. Notice that the time restrictions associated with actions in the second operand will not be considered until its execution begins. ● ref: An InteractionUse refers to a CF. This is merely a shorthand for copying the contents of the referred CF at the point where it is used. We only use them to indicate the interactions that take place as a response to notifications. MATHEMATICAL AND COMPUTER MODELLING OF DYNAMICAL SYSTEMS 575 3.2. WSRF and WSN The WSRF [3] is an OASIS [28] standard, which defines a framework for modelling and accessing persistent resources using Web services. This approach consists of a set of specifications that define the representation of WS-Resources manipulated by Web services. WS-Resources are described by the so-called Resource Properties Documents, which are XML specifications that contain all the relevant resource information. This document is a projection of the actual state of the WS-Resource and serves to define the structure upon which query and update messages are directed. Thus, any operation that manipulates a resource property via the WS-Resource proper- ties document must be reflected in the actual implementation of the WS-Resource’s state. The WSRF standard provides us with operations to read or modify the resource properties, as well as to describe and control the resource lifetime, but no indication is made about the way in which resources are created and made visible. It is assumed that WS-Resources are created by some external mechanism or through the use of a WS-Resource factory, which creates the resource and establishes an association with a Web service, returning an end point reference (EPR), which can thereafter be used to direct requests to the WS-Resource. Resources can be destroyed either by invoking the operation Destroy or because their lifetime has expired. The Destroy operation is equivalent to reassigning the resource lifetime to zero, so we can use this operation as a way to destroy resources. WSRF can be complemented with WSN [6], which defines a set of specifications to standardize the subscription/notification mechanism, with the purpose of allowing clients to subscribe to WS- Resources and be notified about specific changes in the resource state. A Subscribe operation is therefore provided, in which the client indicates the EPR of the resource and the TopicExpression that indicates the condition upon which the notification must be sent. In addition, subscriptions may have a finite duration, after which the subscription is cancelled. There are some other features of WSRF that will not be considered in this paper, such as the insertion and deletion of properties for existing WS-Resources, the aggregation of multiple WS- Resources or Web services into ServiceGroups, or the fault handling mechanisms. 4. UML+WSRFN syntax In this section we first establish the UML+WSRFN model, which captures the main aspects of both UML and WSRF/WSN that have been described in the previous section, after which we define an operational semantics for it. Thus, we will have a graphical representation for the UML +WSRFN model that shows the sequence of messages exchanged among the participants or services involved, as well as the resources they manipulate and the messages used for that purpose. For our purposes, a UML+WSRFN specification is described by the following abstract syntax: U ::¼ðRoles; CF; Vars; GatesÞ; where Roles ¼fg r ; ... ; r are the n participants that make up the system. These are the clients, 1 n services, WS-Resources, and a Registry used for the publishing and discovery of resources. The Registry will always appear in our descriptions, since it is needed as a directory service for the published WS-Resources to provide us with a map between the textual resource names and their respective EPRs. CF describes the high-level behaviour of these participants at the CF level. This is here called the root CF, which will possibly contain other inner CFs, according to the syntax described below. Vars is the set of variables used in this specification, whose values move in specific domains for each variable, and Gates is the set of gates used for the communications involving messages outside the CFs. We represent WS-Resources by using dashed boxes enclosing their names (see Figure 2), and their lifelines are also drawn as dashed lines, instead of dotted ones, and thus they will be clearly identified in the graphical representation. WS-Resources are assumed to be published by some participant, which makes them visible. A publish message is sent 576 V. VALERO AND M.-E. CAMBRONERO sd Creditcard Credit card (CR) :Client :Bank :Registry (WS−Resource) assign(vCR,EPR_CR) publish(vCR,"CR−USER",1000,365) discover("CR−USER",vCCR) getprop(vCCR,balance) send(Bank,200) recv(Client,w) setprop(vCR, + w) Figure 3. A simple UML+WSRFN illustration. to the Registry for this purpose, where a textual tag serves to identify the WS-Resource type, so the clients and other services that need to use a WS-Resource of this class can invoke a discover operation indicating this tag. There can be several distinct implementations of a WS-Resource (e.g. a printing service may be offered using different printers), so the discovery mechanism will only return the EPR of one of them. The arrows pointing to WS-Resources will be labelled with WSRFN messages, representing the requested WSRFN operations affecting this resource, such as getprop or setprop in Figure 3. However, notice that no arrow can leave WS-Resources, because they are here considered as passive entities, whose state can only be queried or changed by the messages that the other participants send. Subscribe is the only operation that could generate notification messages from a WS-Resource when its state fulfils the specified condition. However, due to the asynchronous nature of these notification messages, and taking into account the fact that they will normally be followed by a specific response in the form of a CF, we have decided to omit notification messages and declare instead a CF argument in Subscribe, which is the response behaviour of a notification message corresponding to this subscription. CFs are now formally introduced, according to the following syntax: ðr : A ; .. . ; r : A Þj F ; F j loopðg; FÞj 1 1 n n F ::¼ ; parðF; FÞj altðg ) F;. ..; g ) F; FÞ 1 n where ðr : A ; .. . ; r : A Þ stands for a basic description, in which r ; ... ; r are the roles or 1 1 n n 1 n participants involved, and A ; .. . ; A are the basic interactions they perform, whose syntax is 1 n defined below. The strict sequential composition (strict) is here represented by the classical semicolon operator. Loopðg; FÞ represents the iterative execution of the indicated CF behaviour, as long as the guard g is true, and parðF; FÞ represents the parallel execution of both arguments. Sequential and parallel compositions have been introduced as binary, but they can be easily extended as n-ary, so in the examples we will use their extended versions when necessary. Finally, altðg ) F;... ; g ) F; FÞ represents the alt-CF, in which we have the different alternatives with 1 n their guards, and the final CF corresponds to the else part. This else part is optional, but notice that an empty CF (all roles performing nil) can be used for syntactic completeness in this case, which enables us to avoid us these tedious syntactic distinctions. For the guards g; g ; ... ; g , we allow conditional expressions constructed using the variables 1 n and their data domain values, using the corresponding operators for these domains. We can also use the global clock, referred to as G in the expressions. We now introduce the syntax for the basic interactions (here called activities) performed by the participants, excepting both the Registry and WS-Resources: MATHEMATICAL AND COMPUTER MODELLING OF DYNAMICAL SYSTEMS 577 niljj assignðw; exprÞ; A waitðtÞ;Aajj ðtÞ; A sendði; exprÞ; A j A ::¼ ; recvði; wÞ; Ajj gsendðp; exprÞ; A grecvðp; wÞ; A j A where A are the WSRFN-related activities: publishðEPR; tag; expr; time exprÞ; A j discoverðtag; vEPRÞ; A j setTimeðvEPR; time exprÞ; A j getTimeðvEPR; wÞ; A j A ::¼ ; getpropðvEPR; wÞ; A j setpropðvEPR; exprÞ; A j subscribeðvEPR; cond; time expr; FÞ; A where w; vEPR 2 Vars, expr is an expression possibly constructed by using variables, t and time expr are time expressions, i 2fg 1; .. . ; n (participants), p 2 Gates, EPR is either a natural value or a variable name containing this value, tag is a string, and cond a boolean expression in which the symbol R can be used as representative of the resource property value. Regarding the Registry and WS-Resources, according to our passive interpretation of them, their only possible actions will be those corresponding to the messages sent to them or nil. Thus, following their lifeline we will obtain a sequence of actions, as response to the messages sent, which will be annotated with the invoking role index and finished by a nil action. For instance, for CR in Figure 3 we obtain as behaviour: CR ¼ getprop ðvCCR; balanceÞ; setprop ðvCR; R þ wÞ; nil. C B Nil represents a no-action, and it is used when a participant does not perform any actions. Assignment is clear, waitðtÞ represents a delay of t time units, whereas aðtÞ indicates a behaviour execution a that must start at time t. Notice that timed behaviours with a duration associated can be modelled by using a starting and finishing action and a delay between them: init aðtÞ; waitðdÞ; end aðt þ dÞ: Sendði; exprÞ is used to send the value of expr at the current state to participant r,ina synchronous way, whereas recvði; wÞ is used for a participant to receive a value from participant i, which is stored in variable w. A message can be sent to an external CF by using gates (gsend), and grecv can be used to retrieve messages from the gates. These message transmissions using gates are asynchronous. A WS-Resource is published by invoking the operation publish, indicating the resource EPR as first argument and the type of service in the tag argument. Its initial value and lifetime will respectively be the values of expr and time_expr. A participant that needs to use a resource invokes the discover operation to find a WS-Resource implementing the type of service indicated by the tag argument. As a result, variable vEPR contains the EPR of a published WS-Resource that implements this type of service, or – 1 in the event that no WS-Resource implementing the service has been published. Operations setTime and getTime are respectively used to reassign or get the current resource lifetime. SetTime invoked with time_expr equal to zero will destroy the resource. Thus, we omit a separate Destroy operation, which can be obtained from setTime. Setprop and getprop allow us to modify or read the current resource property value. We assume again that symbol R in the argument expression of setprop denotes the current value of the resource property. Thus, taking integers as property values, an expression such as Rþ2 denotes that its current value is increased by 2. Participants can subscribe to WS-Resources by using the subscribe operation, indicating the subscription condition in cond, which is a resource state-related boolean expression. Symbol R is then used as representative of the resource value, for example, R < 100 can be used for a participant to indicate that he wants to be notified when the resource value is greater than 100. Argument F is the CF that will be performed as notification response when the indicated condition holds. Resources are automatically removed from the system when their lifetime expires, after which any attempt to access the resource generates a failure (the invoking partici- pant is immediately stopped). 578 V. VALERO AND M.-E. CAMBRONERO Example 4.1 A first UML+WSRFN simple example is shown in Figure 3, with four participants: Bank, Client, Registry, and Credit Card (WS-Resource). The Credit Card (CR) is published by the Bank, its property is the current credit available with the card. We can see that the Bank assigns the resource EPR to a variable vCR and publishes the card. The Client then discovers the resource, and gets his current credit (getprop). He eventually deposits € 200 at the Bank (send–recv), after which the Bank updates his credit (setprop) by increasing it by this same amount. An improved version of this example is shown in Figure 4, where the Client now subscribes to the Credit Card resource, asking for a notification when the credit is lower than € 500. The client then repeats the same behaviour, which is to assign variable c (cost of an object he intends to buy) to a randomly selected value in the interval [1,30] (we use a function rand for this purpose), and buying the object if he has got enough credit, which means to update the available credit (setprop) and decrease its variable ‘balance’ by this amount. When notified, the Client checks if he can send € 500 to the Bank, after which the Bank increases the credit by this same amount. 5. UML+WSRFN operational semantics The operational semantics for the UML+WSRFN model is defined on the basis of the two syntactic levels we have introduced (basic interactions and CFs). We first introduce the notation and formal definitions required for this purpose. Definition 1 (States) A state is defined as a tuple s ¼ðG; V; P; ρÞ, where G is the global clock value at this state, V the variable values, P the Gates state, and ρ the global resource state. P captures all the messages sent by using gates, but not yet received. A FIFO message queue q is then associated to each gate p for this purpose, with the classical operations isEmpty, enqueue, top, and dequeue. Thus, P¼ q . p 2 Gates For any gate p 2 Gates, and op 2fg enqueue; dequeue , we define [ for pp ; p 0 0 0 op ðp ; mÞ¼ q ; where q ¼f : P 0 p p p 2 Gates opðq ; mÞ otherwise This captures the new Gates state after the operation op has been performed on q . The resource state ρ is defined as follows: ρ ¼fðEPR ; tag ; value ; lifetime ; Subs Þg ; i i i i i i¼1 where r is the current number of published resources in the system. For each published resource r we register the following information: End Point Reference (EPR ), resource textual i i identification (tag ), actual value at this state (value ), remaining lifetime (lifetime > 0), and i i i subscriber information: Subs ¼fðRole ; expr cond ; Stime ; F Þg i i i i i j j j j j¼1 with i ¼ 1; .. . ; r, and s 2fg 1; ... ; n is the current number of subscribers to resource r . For i i each subscription we register the following information: subscriber (Role ), notification condi- tional expression (expr cond ), subscription remaining time (Stime > 0), and CF that must be i i j j performed when the conditional expression becomes true (F ). Notation: EPR 2 ρ denotes that there is a resource with endpoint reference EPR in ρ (otherwise EPR‚ρ). In a similar way tag 2 ρ denotes that there is at least one resource in ρ with tag value tag (otherwise tag‚ρ). We respectively use ρ ðEPRÞ, ρ ðEPRÞ, and ρ ðEPRÞ to denote the property v t s value, lifetime, and list of subscribers (in ρ) of the resource with reference EPR. We also use the function evalðexpr; sÞ to evaluate an expression at the state s, but in some cases we will just use a MATHEMATICAL AND COMPUTER MODELLING OF DYNAMICAL SYSTEMS 579 sd Creditcard Credit card (CR) :Bank :Client :Registry (WS−Resource) strict assign(vCR,EPR_CR) assign(m,1000) publish(vCR,"CR−USER",1000,365) discover("CR−USER",vCCR) getprop(vCCR,balance) subscribe(vCCR, < 500, 30, Notification) loop [ balance > 0 ] assign(c,rand(1,30)) alt setprop(vCCR, − c) [balance>c] assign(balance,balance−c) sd Notification Credit card (CR) :Bank :Client (WS−Resource) alt [m>500] send(Bank,500) recv(Client,w) assign(m,m−500) setprop(vCR, + w) Figure 4. Credit card example. variable name or expression as representative of its value, when the state is clear from the context. Furthermore, with ρ ½k=EPR (respectively, ρ ½k=EPR) we represent the change of the property v t value (lifetime) of the resource EPR, which is now assigned to k. A similar notation is used to change the variable values: V½expr=w. For any variable w, DðwÞ will denote the domain of data values of w. The removal of a resource with endpoint reference EPR from ρ is denoted by ρ EPR, which means removing the resource tuple with this reference, and consequently all 580 V. VALERO AND M.-E. CAMBRONERO the subscriptions made to this resource. A function Add subsðρ; EPR; Role; expr cond; Stime; FÞ is used to add a new subscriber to a published resource EPR. In the event that the indicated role has already been subscribed to this resource, its old notification condition, subscription time, and CF are replaced by the newly indicated ones. Function Remove subsðρÞ is used to remove those subscriptions from ρ that have been notified (because their associated conditions are true) or their remaining subscription time is zero. We omit their formal definitions as they are straightforward. 5.1. Basic interaction semantics At the activity level of each participant we have two types of transition: 0 0 ðA; sÞ !ðA ; sÞðaction transitionsÞ 0 þ ðA; sÞ! ðA ; s Þðtime elapsing transitionsÞ: Action transitions represent the evolution by performing the action a, whereas time elapsing transitions represent the activity evolution when a unit of time has elapsed without performing any actions. In this latter case, the reached state s is obtained as the following definition indicates. Definition 2 (Time elapsing) 0 0 0 þ 0 For any state s ¼ðG; V; P; ρÞ, the state s ¼ðG ; V ; P ; ρ Þ obtained after a time unit has elapsed is: G ¼G þ 1, that is, the global clock is increased by one. 0 0 V ¼V and P ¼P, that is, both the variables and message queues remain the same. For ρ ¼fðEPR ; tag ; value ; lifetime ; Subs Þg >, in which "i ¼ 1; .. . ; r >: i i i i i i¼1 Subs ¼fðRole ; expr cond ; Stime ; F Þg >, we define: i i i i i j j j j j¼1 0 0 0 ρ ¼fðEPR ; tag ; value ; lifetime 1; Subs Þj lifetime > 1g , where Subs ¼fðRole ; i i i i i i i i¼1 i j expr cond ; Stime 1; F Þj Stime > 1g , i i i i j j j j j¼1 From this definition we can see that those resources whose lifetime has expired are removed from the system, and the same applies to those subscriptions that have expired. The rules defining the action transitions are presented in Tables 1, 2, and 3. Rule (A1) captures the assignment of variable w to the evaluation of expr. Rule (A2) states that action a can only be executed when the global clock has reached value t, and it is immediate, that is, no time elapses when it is performed. Both rules (A3) and (A4) capture the semantics of the send and recv operators at this level, from which we see that, in principle, the roles involved can perform these Table 1. Action transition rules (I). assignðw;evalðexpr;ðG;V;P;ρÞÞÞ (A1) 0 0 Pðassignðw; exprÞ; A; ðG; V; P; ρÞÞ ! ðA; ðG; V ; P; ρÞÞ; where V ¼V½evalðexpr; ðG; V; P; ρÞÞ=w. tG (A2) ðaðtÞ;A;ðG;V;P;ρÞÞ!ðA;ðG;V;P;ρÞÞ sendði;evalðexpr;ðG;V;P;ρÞÞÞ (A3) ðsendði; exprÞ; A; ðG; V; P; ρÞÞ ! ðA; ðG; V; P; ρÞÞ recvði;mÞ (A4) ðrecvði; wÞ; A; ðG; V; P; ρÞÞ ! ðA; ðG;V½m=w; P; ρÞÞforall m 2 DðwÞ gsendðp;evalðexpr;ðG;V;P;ρÞÞÞ (A5) ðgsendðp; exprÞ; A; ðG; V; P; ρÞÞ ! ðA; ðG; V; P ; ρÞÞ; where P ¼ enqueue ðp; evalðexpr; ðG; V; P; ρÞÞÞ: :isEmptyðq Þ p 0 0 (A6) ; where m ¼ topðq Þ, V ¼V½m=w, and P ¼ dequeue ðp; mÞ: p P grecvðp;mÞ 0 0 ðgrecvðp;wÞ;A;ðG;V;P;ρÞÞ!ðA;ðG;V ;P ;ρÞÞ MATHEMATICAL AND COMPUTER MODELLING OF DYNAMICAL SYSTEMS 581 Table 2. Action transition rules (II). EPR‚ρ (R1) publishðEPR;tag;e;tÞ ðpublishðEPR;tag;exp;texpÞ;A;ðG;V;P;ρÞÞ ! ðA;ðG;V;P;ρ ÞÞ 0 fg ðEPR;tag;e;t;;Þ with e ¼ evalðexp; ðG; V; P; ρÞÞ; t ¼ evalðtexp; ðG; V; P; ρÞÞ > and ρ ¼ ρ [ . EPR 2 ρ (R2) fail ðpublishðEPR;tag;exp;texpÞ;A;sÞ!ðnil;sÞ ðEPR;tag;v;t;SÞ2 ρ (R3) discoverðtag;EPRÞ ðdiscoverðtag;wÞ;A;ðG;V;P;ρÞÞ!ðA;ðG;V½EPR=w;P;ρÞÞ tag‚ρ (R4) discoverðtag;1Þ ðdiscoverðtag;wÞ;A;ðG;V;P;ρÞÞ!ðA;ðG;V½1=w;P;ρÞÞ s ¼ðG;V;P;ρÞ;EPR ¼ evalðvEPR;sÞ2ρ^t ¼ evalðtexpr;sÞ > 0 (R5) setTimeðEPR;tÞ ðsetTimeðvEPR;texprÞ;A;sÞ!ðA;ðG;V;P;ρ ½t=EPRÞÞ s ¼ðG;V;P;ρÞ;EPR ¼ evalðvEPR;sÞ2 ρ ^ evalðtexpr;sÞ¼ 0 (R6) setTimeðEPR;0Þ ðsetTimeðvEPR;texprÞ;A;sÞ!ðA;ðG;V;P;ρEPRÞÞ s¼ðG;V;P;ρÞ;EPR¼evalðvEPR;sÞ‚ρ_evalðtexpr;sÞ < 0 (R7) fail ðsetTimeðvEPR;texprÞ;A;sÞ!ðnil;sÞ s¼ðG;V;P;ρÞ;EPR¼evalðvEPR;sÞ2ρ (R8) getTimeðEPR;ρ ðEPRÞÞ ðgetTimeðvEPR;wÞ;A;sÞ !ðA;ðG;V½ρ ðEPRÞ=w;P;ρÞÞ s¼ðG;V;P;ρÞ;EPR¼evalðvEPR;sÞ‚ρ (R9) fail ðgetTimeðvEPR;wÞ;A;sÞ!ðnil;sÞ s¼ðG;V;P;ρÞ;EPR¼evalðvEPR;sÞ2ρ (R10) getpropðEPR;ρ ðEPRÞÞ ðgetpropðvEPR;wÞ;A;sÞ!ðA;ðG;V½ρ ðEPRÞ=w;P;ρÞÞ s¼ðG;V;P;ρÞ;EPR¼evalðvEPR;sÞ‚ρ (R11) fail ðgetpropðvEPR;wÞ;A;sÞ!ðnil;sÞ s¼ðG;V;P;ρÞ;EPR¼evalðvEPR;sÞ2ρ^k¼evalðexpr;sÞ (R12) setpropðEPR;kÞ ðsetpropðvEPR;exprÞ;A;sÞ!ðA;ðG;V;P;ρ ½k=EPRÞÞ s¼ðG;V;P;ρÞ;EPR¼evalðvEPR;sÞ‚ρ (R13) fail ðsetpropðvEPR;exprÞ;A;sÞ!ðnil;sÞ Table 3. Action transition rules (III). s¼ðG;V;P;ρÞ;EPR¼evalðvEP;sÞ2ρ^t¼evalðtexpr;sÞ > 0 (S1) 0 with ρ ¼ Add subsðρ; EPR; Role; c; t; FÞ, where subscribeðEPR;c;t;FÞ ðsubscribeðvEP;c;texpr;FÞ;A;sÞ!ðA;ðG;V;P;ρ ÞÞ Role is the role performing this activity. s¼ðG;V;P;ρÞ;EPR¼evalðvEPR;sÞ‚ρ_t¼evalðtexpr;sÞ0 (S2) fail ðsubscribeðvEPR;c;texpr;FÞ;A;sÞ!ðnil;sÞ actions separately, that is, the sending role executes the transition indicated by rule (A3), whereas the receiving role can get any value m and store it in variable w, as indicated in rule (A4). The actual synchronization and communication between both roles is therefore captured at the CF- level semantics, as we will see later (rule (AF1) in Table 6). Rules (A5) and (A6) define the semantics of gsend and grecv: the first evaluates expr and enqueues its value in q , whereas the latter gets the top value of q (if non-empty), overriding w with this value. Tables 2 and 3 define the WSRF-operator semantics. All of these operations are performed immediately, that is, no time can elapse for them. Rules (R1) and (R2) define the semantics of the publish operator, from which we see that we cannot publish two resources with the same EPR.A fail action is actually obtained in that case, and the invoking role stops. Notice, however, that we can publish two distinct resources with the same tag, as mentioned above in the informal description. Rules (R3) and (R4) define the discover operator semantics, where one of the resources associated to a specific tag is returned, or −1 in the event that there is no such published resource. Other failures leading to the nil activity are caused by any attempt to perform a setTime, getTime, getptop, setprop, or subscribe operation on non-published resources, or when using bad arguments in these calls. The semantics of setTime is defined by rules (R5), (R6) and (R7). Notice from (R6) that the resource is removed from ρ when its lifetime is set to zero. Rules (R8)–(R13) establish the semantics of getTime, getprop, and setprop. Subscription is defined by rule (S1), in which the indicated subscription is inserted into the corresponding resource subscription information. Time elapsing transitions are defined by the rules in Table 4. Only nil, a(t), wait, send, recv, and grecv allow time elapsing. All the remaining basic interactions are immediate. A timed behaviour execution aðtÞ allows time elapsing until the global clock reaches the value t (rule (D2)). In (D3) 582 V. VALERO AND M.-E. CAMBRONERO Table 4. Delay transition rules. (D1) ðnil; sÞ! ðnil; s Þ s¼ðG;V;P;ρÞ;t < G (D2) ðaðtÞ;A;sÞ! ðaðtÞ;A;s Þ t > 1 (D3) ðwaitðtÞ;A;sÞ! ðwaitðt1Þ;A;s Þ (D4) ðwaitð1Þ; A; sÞ! ðA; s Þ (D5) ðsendði; exprÞ; A; sÞ! ðsendði; exprÞ; A; s Þ (D6) ðrecvði; wÞ; A; sÞ! ðrecvði; wÞ; A; s Þ s ¼ðG;V;P;ρÞ; q 2 P; isEmptyðq Þ p p (D7) ðgrecvðp;wÞ;A;sÞ! ðgrecvðp;wÞ;A;s Þ and (D4) the semantics of wait is defined, and time elapsing for both send and grecv is allowed at this level by rules (D5) and (D6). We will therefore enforce synchronization at the CF level (rule (DF1)), not allowing the delay at that level when both parts are ready to synchronize. Notice also that rule (D7) allows time elapsing when no message can be obtained from gate p in grecvðp; wÞ. 5.2. Combined Fragment semantics At the CF level we have the following types of transition: – ðF; sÞ!ðF ; sÞ (null transition) 0 0 – ðF; sÞ!ðF ; s Þ (action transition) 0 þ – ðF; sÞ! ðF ; s Þ (time elapsing transition) Null transitions are used to resolve the alternatives and loops, depending on the guard evaluation. They are also used in a sequence to activate the second operand when all the participants have finished their actions at the first argument. Null transitions will therefore be applied first, to solve the alternatives, loops, and sequences. When no null transition is possible, the action transitions can be performed, and finally, when no null or action evolution can be performed, time elapsing is permitted. The rules defining null transitions are shown in Table 5. In these rules nil denotes an empty CF ðr : nil; .. . ; r : nilÞ. Rule (F1) is therefore used to activate the second operand in a sequence when 1 n the first has terminated. These rules are simple, so no further explanations are required in general, but notice that nondeterminism is introduced by rule (F8), since any of the alternatives whose guard is true can be performed. When no guard is true, the else-part argument is performed (F9). For the CF-action transitions we must now consider notifications. In response to notifications we perform the CF behaviour indicated in the corresponding subscription. We therefore intro- duce the following definition, capturing the CFs that are launched in parallel with the current one in execution as response to the delivered subscription notifications. Definition 3 Let F be a CF and a state s ¼ðG; V; P; ρÞ, with r s ρ ¼fðEPR ; tag ; value ; lifetime ; Subs Þg , and Subs ¼fðRole ; expr cond ; Stime ; F Þg . i i i i i i i i i i i¼1 j j j j j¼1 Table 5. CF-null transition rules. (F1) ððnil; FÞ; sÞ!ðF; sÞ ðF ;sÞ!ðF ;sÞ 1 2 (F2) ðF ;F;sÞ!ðF ;F;sÞ 1 2 evalðg;sÞ¼true (F3) ðloopðg;FÞ;sÞ!ðF;loopðg;FÞ;sÞ evalðg;sÞ¼false (F4) ðloopðg;FÞ;sÞ!ðnil;sÞ (F5) ðparðnil; nilÞ; sÞ!ðnil; sÞ ðF ;sÞ!ðF ;sÞ 1 1 (F6) ðparðF ;FÞ;sÞ!parðF ;F;sÞ 1 1 ðF ;sÞ!ðF ;sÞ 1 1 (F7) ðparðF;F Þ;sÞ!parðF;F ;sÞ 1 1 evalðgi;sÞ¼true;i2f1;...;ng (F8) ðaltðg )F ;...;g )F ;F;sÞ!ðF ;sÞ 1 1 n n i evalðg ;sÞ¼false;"i2f1;...;ng (F9) ðaltðg )F ;...;g )F ;F;sÞ!ðF;sÞ 1 1 n n MATHEMATICAL AND COMPUTER MODELLING OF DYNAMICAL SYSTEMS 583 For each i 2fg 1; ... ; r and for each j 2fg 1; .. . ; s we define N ðF; sÞ and N ðF; sÞ recursively, i i i as follows: (1) For i ¼ 1; j ¼ 1, F if expr cond ¼ false N ðF; sÞ¼ parðF; F Þ otherwise (2) For i ¼ 1; j > 1, N ðF; sÞ if expr cond ¼ false 1 1 j1 j N ðF; sÞ¼ parðN ðF; sÞ; F Þ otherwise 1 1 j1 j Then, we take N ðF; sÞ¼ N ðF; sÞ. 1 1 (3) For i > 1; j ¼ 1, N ðF; sÞ if expr cond ¼ false i1 i N ðF; sÞ¼ parðN ðF; sÞ; F Þ otherwise i1 i (4) For i > 1; j > 1, N ðF; sÞ if expr cond ¼ false i i j1 j N ðF; sÞ¼ parðN ðF; sÞ; F Þ otherwise i i j1 j Then, N ðF; sÞ¼ N ðF; sÞ. i i Finally, we define NðF; sÞ¼ N ðF; sÞ, which is therefore the parallel composition of F with all the other CFs that have been launched as response to notifications. ◼ Table 6 contains the rules defining the CF-action transitions. Rule (AF1) captures the com- munication and synchronization between two roles r and r , where the resulting CF-action i j transition is labelled with the message m. Notifications are not included in this case, since ρ cannot change as a result of a communication. Rule (AF2) defines the single evolution of a role within a CF, by performing some action a, but in this case some notifications can be delivered, in the event of some subscription condition becoming true. Thus, we take the parallel composition of 0 0 0 0 F with all the CFs that must be performed at the new state s , that is, we evolve into NðF ; s Þ, and we remove the subscriptions that have been delivered from ρ . Rule AF3 captures the semantics for sequential composition, and notice that once all roles terminate their actions in F we can apply rule (F1) from Table 5 to activate and execute the actions of the second component. Finally, rules AF4–AF5 capture the parallel execution of both arguments, by interleaving their actions. Time elapsing at the CF level is defined by the rules in Table 7. For a basic CF ðr : A ; ... ; r : 1 1 n A Þ to allow time elapsing (rule (DF1)) it is required that all the activities A are able to do so and n i no synchronization is possible between two activities A , A . Notice that time elapsing cannot i j generate notifications, since no changes in the resource property values have occurred, and the Table 6. CF-action transition rule. sendðj;mÞ recvði;mÞ (AF1) 0 0 0 ðAi;sÞ! ðA i;sÞ ; ðAj;sÞ! ðA j;s Þ ; ij ; where F ¼ðr : A ; .. . ; r : A ; .. . ; r : A ; .. . ; r : A Þ >, and m 1 1 i i j j n n 0 0 ðF;sÞ!ðF ;s Þ 0 0 0 F ¼ðr : A ; .. . ; r : A ; ... ; r : A ; .. . ; r : A Þ: 1 1 i j n n i j 0 0 (AF2) ðA ;sÞ!ðA ;s Þ;asendðj;mÞ;arecvðj;mÞ;"j2f1;...;ng i i ; where F ¼ðr : A ; ... ; r : A ; .. . ; r : A ; .. . ; r : A Þ, a 1 1 i i j j n n 0 0 0 0 00 ðF;sÞ!ðNðF ;s Þ;ðG;V ;P ;ρ ÞÞ 0 0 0 F ¼ðr : A ; .. . ; r : A ; ... ; r : A ; .. . ; r : A Þ, 1 1 i j n n i j 0 0 00 0 s ¼ðG; V; P; ρÞ >, s ¼ðG; V0;P0; ρ Þ, with ρ ¼ Remove subsðρ Þ. 0 0 (AF3) ðF ;sÞ!ðF ;s Þ 1 1 0 0 ðF1;F;sÞ!ðF 1;F;s Þ 0 0 (AF4) ðF ;sÞ!ðF ;s Þ 1 1 0 0 ðparðF ;FÞ;sÞ!ðparðF ;FÞ;s Þ 1 1 0 0 (AF5) ðF ;sÞ!ðF ;s Þ 1 1 0 0 ðparðF;F Þ;sÞ!ðparðF;F Þ;s Þ 1 1 584 V. VALERO AND M.-E. CAMBRONERO Table 7. Time elapsing CF-transition rules. 0 þ ðA ;sÞ! ðA ;s Þ; "i2f1;...;ng and 9i;j;synði;jÞ i 1 i (DF1) ; where 0 0 þ ððr :A ;...;r :A Þ;sÞ! ððr :A ;...;r :A Þ;s Þ 1 1 n n 1 1 1 n n sendðj;mÞ recvði;mÞÞ 0 0 0 synði; jÞ;½ðA ; sÞ!ðA ; sÞ and ðA ; sÞ!ðA ; s Þ: i j i j 0 þ ðF ;sÞ! ðF ;s Þ (DF2) 1 1 1 0 þ ðF ;F;sÞ! ðF ;F;s Þ 1 1 1 0 þ 0 þ ðF ;sÞ! ðF ;s Þ; ðF ;sÞ! ðF ;s Þ 1 1 1 2 1 2 (DF3) 0 0 þ ðparðF ;F Þ;sÞ! ðparðF ;F Þ;s Þ 1 2 1 1 2 subscription conditions can only be based on these values. Rules DF2 and DF3, respectively, capture time elapsing for the sequential and parallel operators at the CF level. In this latter case, both arguments must allow the passage of time. 6. Case studies In this section two case studies are used to illustrate the UML+WSRFN model, with the purpose to cover nearly all the CFs structures considered in UML+WSRFN and the activities inside them. The only element that is not covered by these two examples is the timed activity aðtÞ; A, in which action a must be executed at a precise absolute instant. Thus, their use is limited to specific situations in which absolute times should be used for some concrete actions. The first case study is a laptop online purchase, where the publish/subscribe paradigm is used in order to take advantage of an offer from a seller by using notifications. Interactions of purchase systems have been modelled in some other works [31–33]. Almendros and Iribarne [31] use SDs in order to model database interactions, using a purchase process to illustrate their approach, but they do not distinguish the resources from roles and time restrictions are not considered. Yuan and Fernández [32] present a set of patterns that model shopping carts, products, catalogue, customer accounts, shipping, and invoices by using class and sequence UML diagrams and they indicate how to include security constraints in the model, but not time constraints. Fontauar et al. [33] describe a webshop e-commerce framework using a variant of UML oriented to model product line architectures, without considering time or distinguishing resources. The main difference with our work is that all these works do not consider time constraints, resources, or the publish/subscribe paradigm. The second case study is an e-voting system, in which we illustrate the use of nested CF structures. E-voting systems have been modelled by some research works [29,34,35]. Pilipovic and Babic [34] have designed an e-voting system for particular and specific populations (student population and parliament elections). To illustrate this process, they consider use case, deployment, and SDs in order to design user interactions, components, and interactions among the objects, respectively. Garca-Zamora et al. [35] present a secure e-voting system for medium scale online elections. They implement a security communication protocol against frauds and double voting. The authors include several UML SDs showing the interactions among a set of three objects, but they do not depict the global interactions. Abo-Rizka and Ghounaim [29] present an e-voting system focused on the specific environment and conditions in Egypt. They show several UML SDs capturing the interactions among the different objects in the system. However, as in the first case study, none of these works include the publish/subscribe para- digm, resources, or time constraints, so all of them focus their goals to specific domains. By contrast, our work offers a more general vision of the interactions among the roles or parties involved in a web composition with distributed resources, using the standardization for both the publish/subscribe paradigm and distributed resources, thus facilitating a formal framework using SDs of UML with CFs as the graphical model that allows the user to have a rapid comprehension of the system behaviour. MATHEMATICAL AND COMPUTER MODELLING OF DYNAMICAL SYSTEMS 585 6.1. Online purchase This first case study is an online purchase process (Figure 5). A client is planning on buying a laptop, but she waits for a good offer, since she has got a limited amount of money (m). She discovers two offers from two different online shops, but the price is still too high for her, so she Sd On-line-Purchase :Shop2 :Shop1 :L1 :L2 :CR :Bank :Client :Registry strict Buying gsend(Buying,0) assign(vL1,EP1) publish(vL1,”L1”,950,365) assign(vL2,EP2) publish(vL2,”L2”,980,365) assign(vCR,ECR) publish(vCCR,”CR_USER”,1500,365) assign(bought,false) assign(m,2000) discover(”CR_USER”,vCCR) subscribe(vCCR,R<1000,365,Deposit) getprop(VCCR,Balance) discover(”L1”,vLL1) par subscribe(VLL1, R<=850,365,Purchase) discover(”L2”,vLL2) subscribe(VLL2, R<=850,365,Purchase) wait(10) setTime(vL1,30) setProp(vL1,R*0,7) wait(10) setTime(vL2,15) setProp(vL2,R*0,8) Figure 5. UML+WSRFN model for the online purchase process. 586 V. VALERO AND M.-E. CAMBRONERO Figure 6. Purchase Combined Fragment. decides to wait until a better offer arrives. She then subscribes to both resources in order to be informed as soon as a good offer comes up. Furthermore, she intends to pay by using a credit card, but she is not sure if her current card credit will allow the payment. She therefore makes a subscription to receive a notification when the credit is lower than € 1000, with the intention of increasing her credit, by making a deposit at the Bank. Ten days later the sales period starts, so both shops simultaneously reduce their laptop prices. Shop Sh1 offers Laptop1 for a period of 30 days with a 30% discount, after which this product is withdrawn. Analogously, shop Sh2 offers Laptop2 for a period of 15 days with a 20% discount, and then withdraws the product. The CF Purchase (Figure 6) is activated when either Laptop1 or Laptop2 has a price lower than € 850. In this case, the current prices for the laptop and the card credit are obtained, and a laptop is finally bought if she has enough credit and the price is below € 850. Finally, Figure 7 shows the CF Deposit, which is activated when the card credit is lower than € 1000, in order to increase her balance if she still has enough money for that. Let us now see the corresponding UML+WSRFN algebraic specification for this example. The roles are Shop ; Shop ; L ; L ; Bank; CR; Client and Registry. However, for simplicity we omit WS- 1 2 1 2 Resources and the Registry in the syntax below, taking into account our passive interpretation of them. Variables and gates are easily obtained either from the algebraic description or the UML SDs. The root CF is CF , defined as follows: sys CF ¼ F ; F ; F ; Sys 1 2 3 where MATHEMATICAL AND COMPUTER MODELLING OF DYNAMICAL SYSTEMS 587 Figure 7. Deposit Combined Fragment. 00 00 F ¼ðShop1 : assignðvL1; EP1Þ; publishðvL1; L1 ; 950; 365Þ; nil; 00 00 Shop2 : assignðvL2; EP2Þ; publishðvL 2; L2 ; 980; 365Þ; nil; Bank : assignðvCR; ECRÞ; publishðvCCR; CR USER ; 1500; 365Þ; nil; Client : gsendðBuying; 0Þ; assignðbought; falseÞ; assignðm; 2000Þ; discoverð CR USER ; vCCRÞ; subscribeðvCCR;R 1000; 365; DepositÞ; getpropðvCCR; BalanceÞ; nilÞ F ¼ parðF ; F Þ 2 21 22 F ¼ðShop1 : nil; Shop2 : nil; Bank : nil; 00 00 Client : discoverð L1 ; vLL1Þ; subscribeðvLL1;R 850; 365; PurchaseÞ; nilÞ F ¼ðShop1 : nil; Shop2 : nil; Bank : nil; 00 00 Client : discoverð L2 ; vLL2Þ; subscribeðvLL2;R 850; 365; PurchaseÞ; nilÞ F ¼ðShop1 : waitð10Þ; setTimeðvL1; 30Þ; setpropðvL1;R 0; 7Þ; nil; Shop2 : waitð10Þ; setTimeðvL2; 15Þ; setpropðvL2;R 0; 8Þ; nil; Bank : nil; Client : nilÞ Deposit ¼ altððm > 1000Þ) parðDeposit1; Deposit2Þ; nilÞ Deposit1 ¼ðShop1 : nil; Shop2 : nil; Bank : nil; Client : gsendðgate; 1000Þ; assignðm; m 1000Þ; nilÞ Deposit2 ¼ðShop1 : nil; Shop2 : nil; Bank : grecvðgate; wÞ; setpropðvCCR;Rþ wÞ; nil; Client : nilÞ Purchase ¼ F ; F ; F p1 p2 p3 588 V. VALERO AND M.-E. CAMBRONERO F ¼ðShop1 : nil; Shop2 : nil; Bank : nil; p1 Client : grecvðBuying; 0Þ; getpropðvLL1; PPL1Þ; getpropðvLL2; PPL2Þ; nilÞ F ¼ðaltðð!boughtÞðPPL1 850 & balance PPL1Þ) F ; p2 p21 0:5cmðð!boughtÞðPPL2 850 & balance PPL2ÞÞ ) F ; nilÞ p22 F ¼ðShop1 : nil; Shop2 : nil; Bank : nil; p21 Client : setpropðvCCR;R PPL1Þ; assignðbalance; balance PPL1Þ; assignðbought; trueÞ; nilÞ F ¼ðShop1 : nil; Shop2 : nil; Bank : nil; p22 Client : setpropðvCCR;R PPL2Þ; assignðbalance; balance PPL2Þ; assignðbought; trueÞ; nilÞ F ¼ð Shop1 : nil; Shop2 : nil; Bank : nil; Client : gsendðBuying; 0Þ; nilÞ p3 A gate buying is used to avoid two simultaneous executions of the Purchase CF, which could produce the client to buy two laptops when both shops reduce their prices at the same time. Figure 8 illustrates the main states through which the system evolves along its execution. Doubled circles represent states in which some subscriptions can be active, whereas single circles correspond to states in which no subscription is active. Table 8 shows one possible execution trace of the Purchase System, indicating the action performed, the time at which it has been executed, the SD and the participant that performs the action. Many activities are performed in time 0, since they are immediate, although they are causally related. Should we need to express a duration for some activities, we then would include a wait activity after them. In time 10 both shops reduce the laptop prices, so the Purchase CF is performed twice because the subscription condition is satisfied in both cases. However, the second instance of the Purchase CF must wait until the first one terminates, and thus only one laptop is finally bought. Figure 8. Relevant states of the online purchase. MATHEMATICAL AND COMPUTER MODELLING OF DYNAMICAL SYSTEMS 589 Table 8. Execution trace for the purchase system. Action Time SD Role gsend(Buying, 0) 0 Root Client assign(vL1, EP1) 0 Root Shop1 publish(vL1, ‘Asus’, 950, 365) 0 Root Shop1 assign(vL2, EP2) 0 Root Shop2 publish(vL2, ‘Laptop HP Pavilion’, 980, 365) 0 Root Shop2 assign(vCR, ECR) 0 Root Bank publish(vCCR, ‘CR STEVEN’, 1500, 365) 0 Root Bank assign(bought, false) 0 Root Client assign(m,2000) 0 Root Client discover(‘CR STEVEN’, vCCR) 0 Root Client subscribe(vCCR, R < 1000, 365, Deposit) 0 Root Client getprop(vCCR, Balance) 0 Root Client discover(‘Asus’, vLL1) 0 Root Client subscribe(vLL1, R < 850, 60, Purchase) 0 Root Client discover(‘Laptop HP Pavilion’, vLL2) 0 Root Client subscribe(vLL2, R < 850, 365, Purchase) 0 Root Client wait(10) 0 Root Shop1 wait(10) 0 Root Shop2 setTime(vL1,30) 10 Root Shop1 setprop(vL1, 665) 10 Root Shop1 grecv(Buying, 0) 10 Purchase 1 Client getprop(vLL1, PPL1) 10 Purchase 1 Client getprop(vLL2, PPL2) 10 Purchase 1 Client setTime(vL2,15) 10 Root Shop2 setprop(vL2, 784) 10 Root Shop2 setprop(vCCR, 835) 10 Purchase 1 Client assign(balance, 835) 10 Purchase 1 Client assign(bought, true) 10 Purchase 1 Client gsend(Buying, 0) 10 Purchase 1 Client grecv(Buying, 0) 0 Purchase 2 Client getprop(vLL1, PPL1) 10 Purchase 2 Client getprop(vLL2, PPL2) 10 Purchase 2 Client gsend(gate, 1000) 10 Deposit Client assign(m, m-1000) 10 Deposit Client grecv(gate, 1000) 10 Deposit Bank setprop(vCR, R + 1000) 10 Deposit Bank 6.2. E-voting In this second case study we apply UML+WSRFN to an electronic voting system. There are a number of different ways to implement e-voting systems [30,36,37], and some countries have recently started to use these electronic voting systems, at least partially. In the 1960s punched cards were used in the USA. Other systems based on physical ballots use an optical scanner (OS) to detect the marks the voters have made on the paper. In Brazil a Direct-Recording Electronic voting machine (VM) is used in nearly all votations, and it consists of a touchscreen that shows the candidates, and voters only need to touch the selected option. There are also Internet voting systems, which have been used occasionally, but the non-physical presence of voters generates public concerns about potential government manipulation, so remote voting systems will possibly not be used in federal or national elections, and the physical presence of voters in the polling stations seems to be a firm requirement. Thus, electronic voting systems will more likely be used to help with the counting process rather than to avoid the physical presence of the voters at the polling stations. Furthermore, another primary requirement is the capability of auditing the voting process to detect possible fraud or malfunction. A receipt can be printed out by the VM to fulfil this requirement, but this is subject to problems such as voter intimidations or vote selling, so cryptography or invisible ink have been used to hide the vote on the printed cards. We consider a hybrid model based on some kind of printed voting card (VC), which is printed out by a VM after the voter has been identified and her vote has been provided by some means, 590 V. VALERO AND M.-E. CAMBRONERO such as a touchscreen. The card contains the vote, and it is inserted into an OS that reads it and tallies the results. These printed cards can be modelled by WS-Resources, their property values are the candidates or parties voted for, and they have a finite lifetime, since they must be used immediately after they have been printed out, to avoid possible manipulation. We assume that voters only have 30 min to insert the card into the scanner after it has been printed out. Voters are inscribed (published) by the Administration (Adm) in the electoral roll (Registry) before the election. Thus, for each voter there is an associated WS-Resource (Voter_IDF) which serves to know if she has already voted. The actual behaviour of voters is captured by Voter role, and we also have the VM, and the OS as active roles. VCs are introduced as WS-Resources, and these contain the votes and are only valid for 30 min. At the top of Figure 9 we can see that Adm publishes all the voters, giving them different EPRs. Their initial value is 0 for all of them, indicating that they have not yet voted. Their lifetime is set to a value that overruns the whole votation time. Voters can arrive at the polling station and vote sequentially (a random delay is introduced here) until the global clock reaches the closing time. Each voter is first identified by the VM by using her personal identification number (id_user), which is used to detect (discover) if the voter Figure 9. UML+WSRFN e-voting model. MATHEMATICAL AND COMPUTER MODELLING OF DYNAMICAL SYSTEMS 591 appears in the Registry and to check that she has not yet voted. The voter then selects her vote on the screen and VM publishes the corresponding card (VC), whose value is the candidate voted for, with a lifetime of 30 min. After getting the card, the voter goes to the OS and inserts the card. The OS checks that the card is still valid (discover) and reads the vote from it. Finally, the card is disabled by the OS (removed as WS-Resource) and the voter entry is changed to 1 in order to indicate that she has now voted. Let us now see the corresponding UML+WSRFN algebraic specification for this system, where for simplicity we do not consider the vote storage and the vote recount parts. We omit again in the following description the behaviour for both the Registry and WSRF resources. The root CF is F ¼ F ; F ; F ; . Sys 1 2 3 where F ¼ðAdm : assignðEP; 0Þ; nil; VM : nil; Voter : nil; OS : nilÞ F ¼ðloopðEP 1000; F ÞÞ 2 2;1 F ¼ðloopðG < ClosingTime; F Þ 3 3;1 with 00 00 F ¼ðAdm : assignðV; EPÞ; publishðV; VOTER IDF þ EP; 0; 720Þ; 2;1 assignðEP; EP þ 1Þ; nil; VM : nil; Voter : nil; OS : nilÞ F ¼ F ; F 3;1 4 5 F ¼ðAdm : nil; VM : recvðVoter; idÞ; discoverð VOTER IDF þ id; vVR1Þ; getpropðvVR1; VotedÞ; nil; Voter : waitðrandomÞ; sendðVM; id usrÞ; nil; OS : nilÞ F ¼ altððVoted ¼¼ 0Þ) F ; nilÞ 5 6 F ¼ðAdm : nil; VM : A ; Voter : A ; OS : A Þ 6 VM Voter OS 00 00 A ¼ recvðVoter; ballotÞ; publishðid; VOTER CARD þ id; ballot; 30Þ; VM sendðVoter; 0Þ; nil A ¼ waitðrandomÞ; sendðVM; partyÞ; recvðVM; votecardÞ; waitðrandomÞ; Voter sendðOS; id userÞ; nil A ¼ recvðOS; voter idÞ; discoverð CARD IDF þ voter id; vCard1Þ; OS getpropðvCard1; voted partyÞ; setTimeðvCard1; 0Þ; setpropðvVR1; 1Þ; nil Figure 10 shows the main states through which the system evolves, according to this specifica- tion, and Table 9 a possible trace of the e-voting system. 7. Conclusions and future work In this paper we have presented a formal framework based on UML 2.4.1 SDs with CFs to model Web services with distributed resources. UML 2.0 SDs have been chosen because they allow us to model the sequence of messages exchanged among the different parties in a Web service system. Furthermore, we have benefited from the additional UML 2.4.1 utilities, such as CFs, which allow us to include nested constructions and the main control structures (sequence, loops, alternative, and parallel). Another important contribution of the paper is to enrich these UML SDs modelling timed service and resource relationships, by adding WSRF and WSN derived communications. Thus, we have included timed operators to capture delays or timed restricted behaviours, as well 592 V. VALERO AND M.-E. CAMBRONERO Figure 10. Relevant states for the e-voting system. Table 9. Execution trace for the e-voting system. Action Time Role assign(EP, 0) 0 Adm assign(V, EP) 0 Adm publish(V, ‘VOTER_IDF”+EP, 0, 720) 0 Adm assign(EP, EP+1) 0 Adm times repeated (once for each voter) . . . . . . wait(random) 0 Voter send(VM, id_usr) 40 Voter recv(Voter,id) 40 VM discover(‘VOTER_IDF’+ id,vR1) 40 VM getprop(vR1, Voted) 40 VM wait(random) 40 Voter send(VM, party) 70 Voter recv(Voter, ballot) 70 VM publish(id, ‘VOTER_CARD’+id, ballot, 30) 70 VM send(Voter,0) 70 VM recv(VM, votecard) 70 OS wait(random) 70 Voter send(OS, id_usr) 90 Voter recv(OS, voter_id) 90 OS discover(‘CARD_IDF’+voter_id, VCard1) 90 OS getprop(vCard1, voted_party) 90 OS setTime(vCard1, 0) 90 OS setprop(vVR1,1) 90 OS Repeated until the closing time . . . . . . as the main WSRFN features. The publish/subscribe model has therefore been included, as well as the subscription/notification mechanism, capturing the notification response from a role as a CF that is performed in response to this notification. MATHEMATICAL AND COMPUTER MODELLING OF DYNAMICAL SYSTEMS 593 The main contribution of this paper has been therefore to present and define in a rigorous way the formal framework for UML+WSRFN, providing an operational semantics for the formalism. Our immediate future work is to implement a translation of UML+WSRFN into a well-known formalism (timed automata), with the intention of obtaining a timed automata representation, which can be simulated and analysed by using some existing tools, such as UPPAAL [21]or KRONOS [38]. This work can also be extended by including some additional features related with timed service systems and WS-Resources, such as event and fault handlers. We could also enrich our participant activity model by using more sophisticated business process constructions, for exam- ple, by using WS-BPEL [26] as reference for the activities performed by the roles. Note 1. R in the Figure denotes the resource property value. Disclosure statement No potential conflict of interest was reported by the authors. Funding This work was supported in part by the Spanish Ministry of Science and Innovation and the European Union FEDER Funds with the Project DArDOS entitled Formal development and analysis of complex systems in distributed contexts: foundations, tools and applications under Grant TIN2015-65845-C3, subproject 2-R. References [1] G. Alonso, F. Casati, H. Kuno, and V. Machiraju, Web Services: concepts, Architectures and Applications, Springer-Verlag, Berlin Heidelberg, 2004. [2] OMG. Unified Modeling Language (UML), v2.4.1. http://www.omg.org/spec/UML/2.4.1. [3] OASIS. OASIS web services resource framework (WSRF), v1.2. 2006. https://www.oasis-open.org/committees/ tc_home.php?wg_abbrev=wsrf. [4] M.E. Cambronero and V. Valero. Modeling distributed service systems with resources using UML. International Conference on Computational Science (ICCS’13), Procedia Computer Science (Elsevier), vol. 18, pp. 140–148. 2013. [5] J.C.M. Baeten and C.A. Middelburg. Process algebra with timing. EATCS Monographs Series, Springer- Verlag. 2002. [6] P. Niblett and S. Graham, Events and service-oriented architecture: The OASIS web services notification specifications, IBM Syst. J. 44 (4) (2005), pp. 869–886. doi:10.1147/sj.444.0869 [7] M. Bravetti and G. Zavattaro, Service oriented computing from a process algebraic perspective, J Log Algebr Program 70 (1) (2007), pp. 3–14. doi:10.1016/j.jlap.2006.05.002 [8] R. Mirandola and V. Cortellessa. UML based performance modelling of distributed systems. Proc. 3rd International Conference on the Unified Modelling Language: Advancing on the Standard, UML’00. Lecture Notes in Computer Science, vol. 1939, pp. 178–193. 2000. [9] M. Tribastone and S. Gilmore. Automatic translation of UML sequence diagrams into PEPA models. International Conference on Quantitative Evaluation of Systems (QEST’08), pp. 205–214. 2008. [10] J. Hillston, A Compositional Approach to Performance Modelling, Cambridge University Press, New York, NY, 1996. [11] B. Selic, A generic framework for modeling resources with UML, Comput. journal, IEEE Comput. Soc. . 33 (2000), pp. 64–69. doi:10.1109/2.846320 [12] Y. Lin and B. Plade. Survey of publish-subscribe event systems. Computer Science Department, Indiana University. Technical Report, vol. 16. 2003. [13] R. Baldoni, M. Contenti, S. Tucci, and A. Virgilio. Modelling publish/subscribe communication systems: Towards a formal approach. Proc. 8th IEEE International Workshop on Object-Oriented Real-Time Dependable Systems, pp. 304–311, 2003. [14] D. Garlan, S. Khersonsky, and J.S. Kim. Model-checking publish-subscribe systems. Proc. 10th International SPIN Workshop on Model Checking Software (SPIN’03), pp. 166–180. 2003. 594 V. VALERO AND M.-E. CAMBRONERO [15] Y.B. Hlaoui and L.J.B. Ayed. A model transformation approach based on homomorphic mappings between UML activity diagrams and BPEL4WS specifications of grid service workflows. Proc. IEEE 35th Annual Computer Software and Applications Conference Workshops, IEEE Computer Society, pp. 243–248. 2011. [16] S. Pllana, J. Qin, and T. Fahringer. Teuta: A tool for UML based composition of scientific grid workflows. Proc. First Austrian Grid Symposium, OCG. 2005. http://eprints.cs.univie.ac.at/739/. [17] R. Grønmo and B. Møller-Pedersen, From UML 2 sequence diagrams to state machines by graph transforma- tion, J. Object Technol. 10 (8) (2011), pp. 1–2. doi:10.5381/jot.2011.10.1.a8 [18] M.S. Lund and K. Stølen. A fully general operational semantics for UML 2.0 sequence diagrams with potential and mandatory choice. Proc. 14th International Symposium on Formal Methods (FM’06), LNCS vol. 4085, pp. 380–395. 2006. [19] M.E. Cambronero, V. Valero, and G. Daz, Verification of real-time systems design, In Software Testing, Verification and Reliability 20 (1) (2010), pp. 3–37. doi:10.1002/stvr.405 [20] OMG. UML profile for schedulability, performance, and time specification, v1.1. January, 2005. http://www. omg.org/spec/SPTP/1.1/PDF/. [21] K.G. Larsen, P. Pettersson, and W. Yi, UPPAAL in a nutshell, Int. J. Software Tools Technol. Transfer 1 (1–2) (1997), pp. 134–152. doi:10.1007/s100090050010 [22] M.E. Cambronero, V. Valero, and E. Martnez, Design and generation of web services choreographies with time constraints, J. Universal Comput. Sci. (JUCS) 17 (13) (2011), pp. 1800–1829. [23] N. Kavantzas et al. Web Service Choreography Description Language (WSCDL) 1.0. http://www.w3.org/TR/ ws-cdl-10/(2005). [24] M.E. Cambronero, G. Diaz, E. Martinez, V. Valero, and M.L. Tobarra, WST: a tool supporting timed composite web services model transformation, In Simulation, Transactions of the Society for Modelling and Simulation International 88 (3) (2012), pp. 349–364. doi:10.1177/0037549710372098 [25] J.A. Mateo, V. Valero, and G. Daz. An operational semantics of BPEL orchestrations integrating web services resource framework. Proc. 8th International Workshop on Web Services and Formal Methods, WS-FM 2011. Lecture Notes in Computer Science, vol. 7176, pp. 79–94. 2011. [26] OASIS. Web services business process execution language v2.0. April, 2007. http://docs.oasis-open.org/wsbpel/ 2.0/OS/wsbpel-v2.0-OS.html. [27] I. Foster et al. Modeling stateful resources with web services. Globus Alliance. 2004. [28] OASIS. Adancing open standards for the information society. https://www.oasis-open.org. [29] M. Abo-Rizka and H.R. Ghounaim, A novel in e-voting in egypt, Int. J. Comput. Sci. Netw. Security 7 (11) (2007), pp. 226–234. [30] O.O. Olusola, O.E. Olusayo, O.S. Olantunde, and G.R. Adesina, A review of the underlying concepts of electronic voting, Inf. Knowledge Manag. 2 (1) (2012), pp. 8–21. [31] J.M. Almedros-Jiménez and L. Iribarne, UML modeling of user and database interaction, Comput. J. 52 (3) (2008), pp. 348–367. doi:10.1093/comjnl/bxn028 [32] X. Yuan and E.B. Fernandez, Patterns for business-to-consumer E-Commerce applications, Int. J. Software Eng. Appl. 2 (3) (2011), pp. 1–20. doi:10.5121/ijsea [33] M. Fontaura, W. Pree, and J.B. Rumpe. The webShop E-Commerce framework. Proc. International Conference on Internet Computing (IC’01), pp. 150–156. 2001. [34] D. Pilipovic and D. Babic, A secure e-voting for the student parliament, FACTA UNIVERSITATIS, Electronics and Energetics 29 (2) (2015), pp. 205–218. doi:10.2298/FUEE1602205P [35] C. Garca-Zamora, F. Rodrguez-Henrquez, and D. Ortiz-Arroyo. SELES: An e-voting system for medium scale online elections. Proc. 6th Mexican International Conference on Computer Science (ENC’03), pp. 50–57. [36] ACE Project. E-Voting information. http://www.aceproject.org/ace-en/focus/e-voting/. [37] Internet voting technology alliance. Voting System Requirements. http://www.ivta.org. [38] S. Yovine, Kronos: A verification tool for real-time systems, Int. J. Software Tools Technol. Transfer 1 (1–2) (1997), pp. 123–133. doi:10.1007/s100090050009 [39] OMG. UML profile for marte: Modeling and analysis of real-time embedded systems, v1.1. 2011. http://www. omg.org/MARTE/.
Journal
Mathematical and Computer Modelling of Dynamical Systems – Taylor & Francis
Published: Nov 2, 2017
Keywords: UML 2.4.1; process algebras; WSRF; WS-BaseNotification; distributed resources; distributed systems