throbber
Mobile Agents Coordination in Mobadtl
`
`Gianluigi Ferrari, Carlo Montangero, Laura Semini, and Simone Semprini
`
`Dipartimento di Informatica, Universit`a di Pisa.
`{giangi,monta,semini,semprini}@di.unipi.it
`
`Abstract. We present and formalize Mobadtl, a model for network–
`aware applications, extending the Oikos–adtl temporal–logic based ap-
`proach to the specification and verification of distributed systems. The
`model supports strong subjective mobility of agents under the control of
`stationary guardians. Communications are based on asynchronous mes-
`sage passing. The approach exploits the notions of coordination and re-
`finement to deal separately with the specification of functional issues in
`the agents, and with the specification of coordination policies, e.g. secu-
`rity, routing, etc., in the guardians. The goal is to specify mobile agents
`as independently as possible of the requirements related to the other
`facets of distribution. The specification of an application is obtained by
`instantiating the general model, refining it along different dimensions
`corresponding to the different aspects of interest, and finally composing
`the refinements. The main advantage, besides the increased flexibility of
`the specification process, is that it is possible to specify rich coordina-
`tion policies incrementally, while the functional units remain relatively
`simple. We use Mobadtl to specify a simple electronic commerce applica-
`tion, paying particular attention to the incremental specification of the
`policies. We show how refined policies lead to stronger system properties.
`
`1 Introduction
`
`Present–day network computing technologies exploit mobile entities (either logi-
`cal, like program codes and agents, or physical, like hand–held devices) that exe-
`cute certain computational activities while moving around the network. A basic
`concern in such a context is the complexity of the development of these network–
`aware applications. Network–awareness means that behaviours strongly depend
`on the network environment of the host in which the application is running.
`Moreover, the programming focus is on structural or architectural rather than
`algorithmic issues. The emerging network–aware programming mechanisms and
`languages [15,10] provide effective infrastructures to support forms of mobility
`and control of dynamically loaded software components and physical devices.
`A certain amount of success has been achieved in the development of network–
`aware applications over the WEB; however these experiences have shown the
`difficulties of using traditional software technologies in the context of network–
`aware computing. Therefore, from a Software Engineering perspective there is
`a new challenging issue: the definition of structural and computational models
`to provide designers with conceptual and programming abstractions to master
`
`A. Porto and G.-C. Roman (Eds.): COORDINATION 2000, LNCS 1906, pp. 232–248, 2000.
`c(cid:2) Springer-Verlag Berlin Heidelberg 2000
`
`GOOGLE EXHIBIT 1043
`Google LLC v. Blackberry Ltd.
`IPR2017-01620
`
`Page 1 of 17
`
`

`

`Mobile Agents Coordination in Mobadtl
`
`233
`
`the overall architecture and the structure of the components of network–aware
`applications.
`In this paper we present Mobadtl, a temporal logic based model to specify
`and develop network–aware applications. We introduce the model and its ax-
`iomatic presentation in Oikos–adtl [22], a linear–time temporal logic specifically
`designed to deal with distributed systems with asynchronous communications.
`Our approach is based on the notions of coordination [7,1] and refinement calcu-
`lus [4]. Coordination provides a powerful conceptual tool to specify and develop
`systems in a compositional way. The refinement calculus simplifies the design
`of a system by using incremental development techniques. In Mobadtl, we can
`specify network–aware applications by separating functionality from structural
`design: coordination provides primitives to glue together independent computa-
`tional units, like those realizing the functionalities and those realizing security
`and routing policies. Hence, coordinators are the basic conceptual and program-
`ming abstractions to make applications adapt and react to the dynamic changes
`of their network environments. However, functional specifications cannot ab-
`stract completely from the policies: a policy that does not allow a component
`to enter into a site may have a visible functional effect. Mobadtl provides the
`necessary hooks to provide a very abstract description of the consequences of
`the policies, allowing at the same time to postpone to the appropriate points
`in the refinement process the specific decisions about the policies themselves.
`Indeed, Mobadtl does not provide directly any specific policy: effective policies
`must be explicitly specified through suitable refinement steps.
`To illustrate how Mobadtl supports system specification we consider electronic
`commerce. Electronic commerce has many aspects including security, distribu-
`tion and recovery. It involves strong interaction patterns among the actors (e.g.
`clients and vendors). These are typical features of network–aware applications
`having a set of controlled activities with strong interactions over a distributed en-
`vironment. In the example, we first define the behaviour of a pair of components:
`a customer, and an agent sent to order a pizza, and derive the overall properties
`of the application assuming that the involved sites behave as the generic sites of
`our model. We then refine the application by fixing some policies for these sites,
`and show which new properties of the application can be derived.
`The remainder of this paper is organized as follows. In Section 2, we present
`our abstract model for network–aware computing. Section 3 reviews Oikos–adtl.
`The axiomatization of the model is subsequently defined in Section 4. In Section 5
`we apply the framework to the specification of a simple electronic commerce
`application. We conclude the paper with some remarks about related works and
`future research directions.
`
`2 A Model for Network–Aware Computing
`
`This section presents our abstract model for network–aware computing. First,
`we classify the models for network–aware computing presented in the literature
`along the following axis.
`
`Page 2 of 17
`
`

`

`234
`
`G. Ferrari et al.
`
`The nature of mobile units: They can be any combination of code, data and
`control [15,10]. Models where only pieces of code can be moved are said to
`support a weak form of mobility, while models where the units of mobility are
`processes (code + control) or agents (code + control + data) support strong
`mobility.
`There are programming languages designed only to provide the ability of
`downloading code for execution (e.g. Java [3]). More sophisticated languages
`support migration of entire computations (e.g. Telescript [29]). A number of
`Distributed process calculi have been proposed as formal models for network–
`aware programming. We mention the Distributed Join-Calculus [14], the Dis-
`tributed π-Calculus [18], the Ambient Calculus [6], and the Seal Calculus [28].
`All these calculi advocate programming models which support strong mobility.
`Coordination-based models of behaviours have been adopted in the design of the
`Klaim experimental programming language [11], the σπ calculus [2] and Mobile
`Unity [21]. Klaim extends the Linda [16,8] model with multiple distributed tu-
`ple spaces and provide programming abstractions to support process mobility.
`σπ permits the specification of dynamic networks of components (i.e. networks
`which reconfigure their communication linkages): a component name is the unit
`of mobility. In Mobile Unity the unit of mobility is a component. Program states
`are equipped with a distinguished variable, the location variable, and a change
`of the value of the location variable corresponds to a component migration.
`
`Mobility extent: If not all the components can move, it is useful to distinguish
`between mobile and stationary components. In the Aglets API [19], the aglet
`context provides a bounded environment where mobile components live. Aglet
`contexts are considered as not transferable. Similarly, Telescript’s places are
`stationary components.
`The dichotomy between stationary and mobile components also emerges in
`the foundational calculi. For instance, Klaim’s nodes and Distributed π calculus
`allocated threads are stationary components. In the Ambient calculus, instead,
`ambients are the units of movement and they can be always moved as a whole
`including subambients. However, it is difficult to prove behavioural properties
`of ambients as the control of movements is distributed over all ambients (any of
`them can exercise the movement capabilities). A type system that constraints
`mobility of ambients has been proposed in [5]. Using type information one can
`express whether an ambient is mobile or stationary. To constrain explicitly am-
`bient movements, an extension of the basic calculus has been proposed in [20]:
`the movement interactions become synchronous operations, and any movement
`can take place only if the two participant ambients agree.
`
`Location awareness: The units can be either location aware or not. Location
`awareness results in the ability of choosing between a set of possible next actions
`depending on the current location. Locations reflect the idea of administrative
`domains and computations at a certain location are under the control of a specific
`authority.
`
`Page 3 of 17
`
`

`

`Mobile Agents Coordination in Mobadtl
`
`235
`
`Basically, in all models the units are location aware. The notions of ambi-
`ents in the Ambient calculus, of seals in the Seal calculus, and localities in the
`Distributed Join calculus and Distributed π calculus correspond to variants of
`the general notion of locations. Finally, in Mobile Unity, location awareness is
`modelled by the value hold by the location variable.
`
`Location control: The mobile units can control their location (proactive or subjec-
`tive mobility), or can be moved by other entities (reactive or objective mobility).
`For instance, in Mobile Unity and Klaim only a proactive form of mobility is
`allowed, while the seals are moved by their parent in the Seal calculus. The Am-
`bient calculus is an hybrid: ambients can decide to move, but they carry their
`sub–ambients with them, which are thus moved in an objective way.
`
`Communication model: Examples are the transient shared memory of Mobile
`Unity; the name passing over a named channel in the Distributed Join calculus;
`the anonymous asynchronous message passing via explicit addressing of Klaim.
`In general, remote interactions are handled through explicit naming: a com-
`ponent which interacts over a non-local channel has to know the place where
`the channel is located. An exception to this schema is the Ambient calculus:
`the knowledge of an ambient name is not enough to access its services; it is
`necessary to know the route to the ambient. Finally, interposition mechanisms
`(wrappers), which encapsulate components to control and monitor communica-
`tions have been exploited in [27]. Wrappers support the enforcement of secu-
`rity properties by constraining communications between trusted and untrusted
`components: wrappers explicitly specify which are the allowed communications
`among components.
`
`In our model, a system is based on an immutable net of elaboration nodes:
`the neighborhoods. The neighborhood is a bounded environment where several
`components (both stationary and mobile) live. Components have a unique name,
`e.g. determined by the initial neighborhood and a suffix to distinguish siblings.
`The notion of neighborhood basically corresponds to that of location. Each
`neighborhood is associated with a stationary component, the guardian. The
`knowledge of their own guardian makes components (both stationary and mo-
`bile) location aware. A guardian acts as an interposition interface among compo-
`nents and neighborhoods: it specifies and implements communication and move-
`ment policies. In other words, guardians monitor the components and limit the
`resources they can use. More precisely, communications between components
`occur via the guardians. Communications are based on asynchronous message
`passing. Guardians provide also routing facilities to forward messages and to
`handle migrating components.
`The model supports strong mobility and mobility is subjective, but compo-
`nent migration requests can be refused by guardians, for instance because of
`security reasons. Indeed, guardians intercept messages and components and can
`decide which messages and components can enter or leave the neighborhood they
`control. The following figure provides a pictorial representation of our model.
`
`Page 4 of 17
`
`

`

`236
`
`G. Ferrari et al.
`
`
`
`
`
`
`
`
`
`
`
`
`
`
`
`
`guardian
`
`component
`
`neighborhood
`
`communication
`
`Fig. 1. Communication among components in different neighborhoods: messages and
`migrating components are routed via the guardians at both ends. Which other guardian
`may be involved is fixed by the routing and security policies at lower refinement steps.
`
`The notion of neighborhood permits to model several crucial issues of network–
`aware programming. For instance a neighborhood can be used to represent an
`administrative domain where components are under the control of a single au-
`thority (the guardian), a naming domain where components adopt a given nam-
`ing policy, and also an address space. The current notion of neighborhood is not
`complete. For instance, important requirements are not covered: the ability to
`define new neighborhoods and merge existing neighborhoods is missing.
`Asynchronous communication permits to keep the model abstract from any
`specific communication protocol. The model itself does not embody any routing
`or security policy for the communications between guardians. Effective routing
`and security policies must be explicitly specified through suitable refinement
`steps. The development approach deals separately with functional, security, and
`mobility issues. For instance, we can fully specify the functionality of a com-
`ponent by giving only very abstract description of the security requirements. A
`complete system specification is therefore obtained by plugging together different
`refinements corresponding to different aspects of the system.
`
`3 Background: Oikos–adtl
`
`Oikos–adtl is a specification language for distributed systems based on asyn-
`chronous communications. It is based on an asynchronous, distributed, temporal
`logic, which extends Unity [9] to deal with components and events.
`The language, its semantics, and a number of theorems have been introduced
`in [22,26]. We recall here the most important concepts.
`
`The Computational Model. A system is characterized by a list of component
`names, and a set of state transitions, each associated to a component. A compu-
`tation is a graph of states like the one in the figure below (dotted arrows denote
`multiple transition steps, plain arrows single transitions or message emission).
`Any state of component M is either the result of the application of a local tran-
`sition, (as the one establishing q in the figure below), or the result of a send
`operation originated in a distinguished component (as message r).
`
`Page 5 of 17
`
`

`

`Mobile Agents Coordination in Mobadtl
`
`237
`
`locally
`establish q
`
`// p, q
`
`// p
`
`establish
`r in N
`
`M : p
`N :
`
`// p
`// o
`
`))RRRRRR
`// o, r
`
`Syntax and Semantics. A specification consists of a set of component names, and
`a set of formulae. Formulae are built over state formulae, which express prop-
`erties of single computation states. They shape M : p, where M is a component
`name and p a 1st order logic formula. Formulae describe computations relating
`state formulae by the temporal operators causes c, causes, needs, because c,
`because, when, and those of Unity. Formulae are interpreted on computations.
`Transitions and communications define the next state relation: its reflexive and
`transitive closure define the future state relation. Formulae shape like:
`
`(1)
`(2)
`(3)
`(4)
`
`M : p when c causes (S : q ∧ M : r)
`S : q when c because (S : r ∧ M : p)
`M : q causes N : r
`S : q needs S : c
`An event occurs when a given property is established, i.e. it becomes true. State
`formulae preceding the temporal operators are to be read as events. The con–
`(dis–)junction of state properties following the temporal operators are called
`conditions: for instance, in (3) operator causes relates an event and a condition,
`and specifies that the establishment of q in M is sufficient to let r hold in the
`future in N. because also relates an event and a condition, and specifies that
`the condition is necessary for the event to occur: it must hold before the event
`occurs. needs requires a condition to hold when an event occurs. Finally, when
`is used to express more sophisticated properties, by subjecting the effects of an
`event to additional conditions. For instance, (1) states that any state of M in
`which c holds and p is established is followed by states of S and M satisfying,
`respectively, q and r, as in the computations to the left, below. Formula (2)
`states that q can be established in S when c holds only if previously r and p
`have hold in S and M, respectively, like in the computation to the right. The
`same computation satisfies also (4): when q is established in S, c must hold.
`// c,¬p
`
`M :
`S :
`
`// c, p
`
`//  // r
`// // q
`
`M :
`S :
`
`// p
`
`// r
`
`//  //
`// c, q
`
`// c,¬q
`
`Suffix c stands for closely: causes c requires the condition to occur in the same
`state in which the event occurs, or in the next one; because c requires that the
`condition enabling the event happened in the close past, i.e. in the same (like
`needs ) or in the previous state.
`
`Addressing readability in specifications, we avoid explicit quantifications [26]:
`variables in the premises of a formula (before the temporal operator) are univer-
`
`Page 6 of 17
`
`//
`//
`//
`//
`//
`

`

`238
`
`G. Ferrari et al.
`
`sally quantified, while those appearing free in the conclusions are existentially
`quantified. Finally, a large set of theorems is available to be used to reason on
`Oikos–adtl specifications. Two interesting examples are a weak form of transi-
`tivity for causes (5), and when elimination (6):
`
`M : A causes O : C
`
`O : C causes N : B
`M : A causes N : B
`M : A when ¬B causes O : C2
`M : A when B causes N : C1
`M : A causes N : C1 ∨ O : C2
`
`O : C because M : A
`
`(5)
`
`(6)
`
`4 Axiomatization
`
`The goal of the axiomatization is to capture the most general model which sat-
`isfies the properties of Sect. 2 and to provide the necessary hooks to specify ap-
`plications as refinements of the axioms. In particular we want to deal separately
`with the specification of functional issues in the agents, and the specification
`of coordination policies in the guardians. Thus, the axioms fix an “interface”
`for agents and guardians. This permits to specify applications by instantiating
`the axioms and then adding sets of formulae which state the application specific
`functionalities and the communication and security policies in use. These sets
`can be defined independently of each other.
`In the axioms, location awareness is encoded in the component state via pred-
`icate guardedby(G), which identifies the current guardian, i.e. the current loca-
`tion. Stationary components are characterised by the invariance of this predicate.
`Dually, each guardian holds a representation of the neighborhood it controls via
`two mutually exclusive predicates, guarding(A) and moving(A, T): one of these
`predicates always holds in the guardian for each mobile component (agent, for
`short) which ever entered the neighborhood.
`To move to another neighborhood, an agent A issues a mobility request
`to its guardian. If no veto is raised (events veto( )), the successful movement
`of an agent A to location T is represented by a suitable coordination of the
`events guardedby(T) in the agent and guarding(A) in the guardian T . Predicate
`moving(A, T) identifies those agents that asked to leave the neighborhood and
`are not back yet. To guarantee the correct behavior, the mobility requests of
`agents that already asked to move, are intercepted and the originator is notified
`by double req. Similarly, to send a message, a component sends a communication
`request to the guardian of the neighborhood it currently belongs to. If no veto is
`raised and the message is delivered, delivery occurs via the receiver’s guardian.
`The general model (hence the axioms in this section) does not describe how
`messages or agents reach their target, or why and where a veto is raised: the
`axioms only make clear that any of the guardians involved in a communication
`or a movement, can veto it. Also, the guardians at both ends are necessarily
`involved. Which other guardians may be involved, is fixed by the routing and
`
`Page 7 of 17
`
`

`

`Mobile Agents Coordination in Mobadtl
`
`239
`
`security policies at lower refinement levels. The formulae introduced there detail
`the guardians, and take care of what happens in between the sender and target
`guardians, who raises vetoes, and why.
`In particular, the general axioms do not describe how to deliver a message to
`a moving target. However, they imply that any refinement either guarantees the
`control stabilization property (i.e. that any message actually reaches its target,
`if not vetoed) or has ways to stop tracing a target which is moving too fast, and
`eventually notify a veto (e.g. after a given number of hops between guardians).
`Another issue which is left unspecified in the general model is how vetoes are
`routed: the model only requires that vetoes are delivered. A first realistic refine-
`ment could impose that also vetoes are delivered via the destination guardian.
`Finally, the general model is insecure, and malicious agents could fake vetoes or
`communication and mobility requests wrapping them in messages. Again, the
`specification of suitable safety properties to avoid these misbehaviours is left to
`further refinements.
`
`4.1 Communications
`When a component S needs to send a message M to component R, the event
`communication request msg(M, S, R) is raised in G, the guardian of the neigh-
`borhood S currently belongs to. The request can either succeed, i.e. the message
`is delivered to the receiver, or fail, in which case a veto is notified to the sender.
`If the request is successful, delivery occurs via the receiver’s guardian.
`The top of Table 1 displays the communication liveness axioms. CL1: event
`out(M,R) in S represents the agent’s need to communicate and causes a request
`msg(M, S, R) to the agent’s guardian G, to handle the communication. CL2:
`there are two possible consequences of an event in G which carries the request
`to handle a message for an agent G is not currently guarding. Either there is
`(cid:3) that in a future state will be guarding the receiver and serve
`a guardian G
`the request, or a veto is raised. The first case calls for control stabilization, as
`mentioned above. The second case takes care of the model assumption that any
`guardian involved in a communication can stop it, raising a veto. Vetoes can
`originate similarly in other axioms, and are no longer discussed. CL3: when a
`
`Table 1. Axioms for communications
`
`CL1: S: out(M, R) when guardedby(G) causes G: msg(M, S , R)
`CL2: G: msg(M, S, R) when ¬ guarding(R) causes
`G(cid:2): (msg(M, S, R) ∧ guarding(R)) ∨ S: veto(msg(M, S, R))
`CL3: G: msg(M, S, R) when guarding(R) causes c
`R: in(M, S) ∨ S: veto(msg(M, S, R))
`CS1: R: in(M, S) because c G: (msg(M, S, R) ∧ guarding(R))
`CS2: S: veto(msg(M, S, R)) because G: msg(M, S, R)
`CS3: G: msg(M, S, R) because
`S: (out(M, R) ∧ guardedby(G)) ∨ G(cid:2): (msg(M, S, R) ∧ G (cid:4)= G(cid:2))
`
`Page 8 of 17
`
`

`

`240
`
`G. Ferrari et al.
`
`guardian receives and accepts a message for a component it is guarding, it deliv-
`ers the message (in(M, S)). causes c is needed to force the guardian to deliver
`the message before reacting to a possible movement request by the receiver R.
`The last axioms in Table 1 express communication safety properties. CS1:
`components receive messages only if their guardian received a message delivery
`request. CS2: communication requests are vetoed only if some guardian received
`a message delivery request. CS3: guardians receive communication requests only
`if a component in its neighborhood attempted to send a message or another
`guardian forwarded the request.
`
`The following property holds: G: msg(M, S, R) because S: out(M, R). The proof
`exploits the second disjoint in CS3 and because transitivity, to connect G and
`the guardian of the sender, where the first disjoint of CS3 applies. The proof
`is an interesting example of well–founded recursion: the chain of intermediate
`guardians must be finite, since time is limited in the past. By because transitivity,
`it follows from CS1 and the property above that there are no spurious messages:
`R: in(M, S) because S : out(M, R).
`
`4.2 Mobility
`
`When agent A decides to move to a target neighborhood T , it notifies a mobility
`request to(A, T) to its guardian O, which can either veto or accept the request.
`If the origin guardian O allows the agent to attempt to leave the neighborhood
`it controls, the mobility request may reach the destination neighborhood, or be
`vetoed along the route. If it reaches the destination, the target guardian can still
`reject the request instead of taking the agent under its own control.
`Table 2 lists the mobility liveness axioms. ML1: event moveTo(T) in A rep-
`resents its commitment to move to T . The reaction to this event is a mobility
`request (to(A, T )) to the current guardian O. ML2: guardians immediately record
`(causes c) mobility requests from the agents they are guarding (O: moving(A,
`T)). This “freezes” the requesting agents, and prevents their guardians from con-
`sidering other mobility requests from the same agent, before the current request
`
`Table 2. Axioms for mobility: liveness
`
`ML1: A: moveTo(T) when guardedby(O) causes O: to(A, T)
`ML2: O: to(A, T) when guarding(A) causes c O: moving(A, T)
`ML3: O: to(A, ) when moving(A, ) causes A:double req
`ML4: O: moving(A, T)) causes
`T: from(A, O) ∨ (O: guarding(A) ∧ A: veto(mob(A, O, T)))
`ML5: T: from(A, O) causes (T: guarding(A) ∧ A: guardedby(T)) ∨
`(O: guarding(A) ∧ A: veto(mob(A, O, T)))
`ML6: C: guardedby(G(cid:2)) when guardedby(G) ∧ G(cid:4)=G(cid:2) causes c
`C: ¬ guardedby(G)
`
`Page 9 of 17
`
`

`

`Mobile Agents Coordination in Mobadtl
`
`241
`
`Table 3. Axioms for mobility: safety
`
`MS1: A: veto(mob(A, O, T)) because O: to(A, T)
`MS2: O: to(A, T) because A: moveTo(T) ∧ guardedby(O)
`MS3: O: moving(A, T) because c O: to(A, T)
`MS4: T: from(A, O) because O: moving(A, T)
`MS5: T: guarding(A) because T: from(A, )
`MS6: A: guardedby(G) unless guardedby(G(cid:2))
`MS7: A: guardedby(G) because G: guarding(A)
`MS8: A: double req because O: moving(A, )
`inv ¬ (guarding(A) ∧ moving(A, ))
`MS9: G:
`MS10: G: stable (guarding(A) ∨ moving(A, ))
`inv ¬ guardedby( )
`MS11: G:
`MS12: for all g and c, c initially in g’s neighborhood
`init guarding(c) ∧ from(c, ) and
`g:
`init guardedby(g) ∧ moveTo(g)
`c:
`
`is handled. Indeed, ML3 states that a request from a frozen agent causes a veto of
`the kind double req: safety axioms guarantee that only a frozen agent can cause
`a request to leave O, when O is not guarding A, i.e. only a frozen agent can cause
`the event in ML3. ML4: a mobility request may be forwarded, or may result in a
`veto, as usual. If the request is vetoed, the agent is unfrozen, and returns under
`the control of the origin guardian. ML5: if a request to enter neighborhood T is
`accepted, the guardian starts controlling the requesting agent (T: guarding(A)),
`which enters the neighborhood (A: guardedby(T)). ML6: when an agent changes
`neighborhood, the data recording its old location are immediately removed.
`The general form veto(mob(A, O, T )) permits to accommodate vetoes gener-
`ated in the refinements by intermediate guardians.
`
`Mobility safety conditions are in Table 3. MS1: agents receive mobility vetoes
`only if a guardian handled their request to move. MS2: guardians receive mobility
`requests from an agent they are guarding, only if the agent actually requested to
`move. MS3: guardians handle mobility requests only if they received them. MS4:
`guardians receive mobility requests by agents they are not guarding only if the
`origin guardian accepted the request. MS5: guardians control only agents that
`previously asked to move in. MS6: agents are always aware of their location, i.e.
`of the guardian that guards them. MS7: agents can enter a neighborhood only if
`accepted by the guardian. MS8: mobility requests are considered double only if
`one is actually pending. MS9 and MS10: once an agent entered a neighborhood,
`the guardian always either guards it or serve a mobility request of its, but not
`both at the same time; also, guardians keep track of the agents that left. The
`interplay of guarding, moving and guardedby is such that the model does not
`constrains implementation choices with respect to mobility. E.g. there is no need
`to stop the execution of a frozen agent immediately after a request to move:
`the implementation can wait to do so until permission to leave is granted by
`
`Page 10 of 17
`
`

`

`242
`
`G. Ferrari et al.
`
`the local guardian. The model has nothing to say on the local computations
`in the meantime. It only entails that communication and mobility requests of
`a frozen agent are dealt with differently: communications are regularly served,
`while mobility attempts are captured as double requests. MS11: guardians are
`not guarded, i.e. they are not location aware. MS12: in the initial state, every
`guardian knows the agents it is controlling, and every agent knows the name of
`its guardian. The other terms are needed to fulfill the other safety conditions in
`the initial state.
`The next section gives an example of independent specification of function-
`ality and policy, and of their composition.
`
`5 A Simple Example
`
`This section shows how Mobadtl supports the specification of network–aware
`applications. We specify a simple electronic commerce application where some
`activities strongly interact in a distributed environment. We focus on the coor-
`dination, communication and mobility concerns which guide the design phases.
`To demonstrate how Mobadtl supports the composition of specifications ad-
`dressing different concerns, we specify independently the functionality of the
`system (i.e. the components) and the coordination policies, i.e. the constraints
`on the guardians. We show that the coordination policies lead to stronger prop-
`erties of the system, namely that some vetoes which are possible in the general
`model, no longer arise when the policies are in place. Finally, since the exam-
`ple is very simple (only two neighborhoods), there is no need to specify routing
`policies: should the system be expanded, routing policies could also be added.
`
`5.1 Functional Description
`
`In our scenario, a hungry customer sends an agent to buy a pizza: if allowed to
`enter the shop, the agent will buy the pizza and, once back home, inform the
`customer of the delivery time. Otherwise, the customer will be informed of the
`failure. The involved components are the customer c, a stationary component
`belonging to the Home neighborhood; the agent a, initially in the Home neigh-
`borhood; the guardian of the Home neighborhood h; the guardian of the Shop
`neighborhood s, which plays the role of the shopkeeper.
`We omit to instantiate the general axioms to this particular system and just
`give the formulae to describe the functionalities of the components. Formulae
`c1 and c2 in Table 4 define the customer’s behavior. When the hungry event
`occurs, a message is sent to the buyer agent (out(buy pizza, a)). The second
`formula states that c is stationary.
`The remaining formulae describe the behavior of the agent. a1: a reacts to a re-
`quest from the customer (in(buy(i), c)) committing to move to the Shop neigh-
`borhood. a2 and a3: once in the Shop, the agent records the result of its request
`(delivery at(T)) and goes back Home; once at Home, it communicates the deliv-
`ery time to the customer. a4: the agent will inform the customer if not allowed
`
`Page 11 of 17
`
`

`

`Mobile Agents Coordination in Mobadtl
`
`243
`
`Table 4. Specification of the customer c and the agent a
`
`c1 c: hungry causes c: out(buy pizza, a)
`c2 c: inv guardedby(h)
`a1 a: in(buy pizza, c) causes a: moveTo(s)
`a2 a: guardedby(s) causes a: (delivery at(T) ∧ moveTo(h))
`a3 a: guardedby(h) when delivery at(T) causes a: out(pizza at(T), c)
`, )) causes a: out(failure, c)
`a4 a: veto(mob(a,
`a5 a: delivery at(T) needs guardedby(s)
`a6 a: delivery at(T) unless out(pizza at(T), c)
`a7 a: out(failure, c) because a: veto(mob(a,
`, ))
`
`to accomplish this task (out(failure, c)). a5 and a6 express safety conditions: the
`former states that the event delivery a

This document is available on Docket Alarm but you must sign up to view it.


Or .

Accessing this document will incur an additional charge of $.

After purchase, you can access this document again without charge.

Accept $ Charge
throbber

Still Working On It

This document is taking longer than usual to download. This can happen if we need to contact the court directly to obtain the document and their servers are running slowly.

Give it another minute or two to complete, and then try the refresh button.

throbber

A few More Minutes ... Still Working

It can take up to 5 minutes for us to download a document if the court servers are running slowly.

Thank you for your continued patience.

This document could not be displayed.

We could not find this document within its docket. Please go back to the docket page and check the link. If that does not work, go back to the docket and refresh it to pull the newest information.

Your account does not support viewing this document.

You need a Paid Account to view this document. Click here to change your account type.

Your account does not support viewing this document.

Set your membership status to view this document.

With a Docket Alarm membership, you'll get a whole lot more, including:

  • Up-to-date information for this case.
  • Email alerts whenever there is an update.
  • Full text search for other cases.
  • Get email alerts whenever a new case matches your search.

Become a Member

One Moment Please

The filing “” is large (MB) and is being downloaded.

Please refresh this page in a few minutes to see if the filing has been downloaded. The filing will also be emailed to you when the download completes.

Your document is on its way!

If you do not receive the document in five minutes, contact support at support@docketalarm.com.

Sealed Document

We are unable to display this document, it may be under a court ordered seal.

If you have proper credentials to access the file, you may proceed directly to the court's system using your government issued username and password.


Access Government Site

We are redirecting you
to a mobile optimized page.





Document Unreadable or Corrupt

Refresh this Document
Go to the Docket

We are unable to display this document.

Refresh this Document
Go to the Docket