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 deliver