We introduce and study a prototyping language for describing real-time distributed systems. Its time constraints are expressed as bounded intervals to model the uncertainty of the delay in migration and communication of agents placed in the locations of a distributed system. We provide the operational semantics, and illustrate the new language by a detailed example for which we use software tools for analyzing its temporal properties.
Computer systems today are interconnected into
large distributed systems. Distributed and
concurrent systems are now used in both academic and
industrial computing, forcing researchers and
practitioners to look for theoretical models and software
tools ref ecting the new framework based on mobility
and interaction. Programming paradigms have
progressed, allowing programmers to implement
software in terms of high level abstractions. In distributed
systems, such implementations are given by taking
care of time scheduling, access to resources, and
interaction among processes. When solving problems
in distributed systems, it is useful to have an explicit
notion of location, explicit migration, local
interaction/communication and resource management.
Aiming to bridge the gap between the existing
theoretical approach of process calculi and
forthcoming realistic programming languages for distributed
systems, we have introduced and studied a rather
simple and expressive formalism called TIMO as a
simplif ed version of timed distributed pi-calculus
The paper is organized as follows: Section 2 presents the syntax and semantics of rTIMO using interval constraints. Section 3 provides an example, while Sections 5 and 6 contain the modelling and verif cation in UPPAAL . Finally, Section 7 presents the related work and concludes the paper. 2. SYNTAX AND SEMANTICS OF RTIMO The prototyping language rTIMO provides suff cient expressiveness to model in an elegant way the migration and communication in real-time distributed systems. In this paper we present a revised/improved version of rTIMO involving global timing constraints in which the timing constraints are expressed as intervals in order to model the uncertainty of the delay in migration and communication. This realistic approach is used to provide systems a larger degree of non-determinism, for instance in deciding when a process is allowed to move from one location to another one. We achieve this by assuming that a rTIMO migration process can move to another location during a time interval (and not necessarily after exactly a given number of
P, Q ::= a[t1,t2]!hvi then P else Q p a[t1,t2]?(u) then P else Q p go[t1,t2]l then P p 0 p id(v) p P | Q (output) (input) (move) (termination) (recursion) (parallel)
L Systems
N ::= l[[P ]] ::=
L p L | N time units). Two processes may communicate only if they are present at the same location, they use the same channel and the time constraints allow them to interact.
In rTIMO , the transitions caused by performing actions with timeouts (migration and communication) are alternated with continuous transitions (timepassing). The semantics of rTIMO is provided by multiset labelled transitions in which multisets of actions are executed in parallel (in one step).
Timing constraints expressed as intervals allow to model the uncertainty of the delay in migration and communication. The syntax of rTIMO is given in Table 1, where the following is assumed: • a set Loc of locations l, a set Chan of communication channels a, and a set Id of process identif ers (each id ∈ Id has its arity mid); • for each id ∈ Id there is a unique process def nition id(u1, . . . , umid) def Pid, where the = distinct variables ui are parameters; • [t1, t2], where t1, t2 ∈ R+ and t1 ≤ t2 is an execution time interval of an action; • u is a tuple of variables; • v is a tuple of expressions built from values, variables and allowed operations. • a time interval [t1,t2] associated with a migration action such as go[t1,t2]loc then P indicates that process P can move to location loc after t time units, where t ∈ [t1, t2]. • a time interval [t1,t2] associated with an output communication process a[t1,t2]!hzi then P else Q makes the channel a available for communication (by sending z) for a period of t2 − t1 time units, but only after an idling of t1 time units. It is also possible to impose an interval for an input communication process a[t1,t2]?(x) then P else Q along a channel a. In both cases, if the interaction does not happen in the interval [t1, t2], the process gives up and continues as the alternative process Q.
The only variable binding constructor is a[t1,t2]?(u) then P else Q; it binds the variable u within P , but not within Q. The free variables of a process P are denoted by f v(P ); for a process def nition, it is assumed that f v(Pid) ⊆ {u1, . . . , umid}, where ui are the process parameters. Processes are def ned up-to an alpha-conversion, and {v/u, . . .}P denotes P in which all free occurrences of the variable u are replaced by v, eventually after alpha-converting P in order to avoid clashes.
Since location l, provided by a process go[t1,t2]l then P , can be a variable, its value can be assigned dynamically through communication with other processes; this means that migration supports a f exible scheme for the movement of processes from one location to another. Thus, the behaviour can be adapted to various changes of the distributed environment. Processes are further constructed from the (terminated) process 0, and parallel composition P | Q. A located process l[[P ]] specif es a process P running at location l, and a system N is built from its components L. A system N is well-formed if there are no free variables in N . Remark 1 In order to focus on the mobility and local interaction aspects of rTIMO , we abstract from arithmetical operations, considering by default that the simple ones (comparing, addition, subtraction) are included in the language.
The f rst component of the operational semantics of rTIMO is the structural equivalence ≡ over • systems. The structural equivalence is the smallest congruence such that the equalities of Table 2 hold. (NNULL) N | l[[0]] ≡ N (NCOMM) N | N ′ ≡ N ′ | N (NASSOC) (N | N ′) | N ′′ ≡ N | (N ′ | N ′′) (NSPLIT) l[[P | Q]] ≡ l[[P ]] | l[[Q]] Essentially, the role of ≡ is to rearrange a system in order to apply the rules of the operational semantics given in Table 3. Using the equalities of Table 2, a given system N can always be transformed into a f nite parallel composition of located processes of the form l1[[P1]] | . . . | ln[[Pn]] such that no process Pi has the parallel composition operator at its topmost level. Each located process li[[Pi]] is called a component of N , and the whole expression l1[[P1]] | . . . | ln[[Pn]] is called a component decomposition of the system N .
step of length t ∈ R+.
The operational semantics rules of rTIMO are presented in Table 3. The multiset labelled transitions of
Λ form N −→ N ′ use a multiset Λ to indicate the actions executed in parallel in one step. When the multiset Λ contains only one action λ, in order to simplify the
{λ} λ notation, N −−→ N ′ is simply written as N −→ N ′.
t N ′ represent a time In rule (MOVE0), the process go[0,t]l′ then P migrates from location l to location l′ (illustrated by the label l ⊲ l′ of the transition) and then evolves as process P . In rule (COM), an output process a[0,t]!hvi then P else Q located at location l, succeeds in sending a tuple of values v over channel a to process a[0,t′]?(u) then P ′ else Q′ also located at l.
Both processes continue to execute at location l, the f rst one as P and the second one as {v/u}P ′. The label {v/u}@l of the rule (COM) illustrates the fact that a communication that lead to the replacement of u by v (denoted by {v/u}) took place at location l (denoted by @l). If a communication action has a timer equal to [0, 0], then by using the rule (PUT0) for output action or the rule (GET0) for input action, the generic process a[0,0] ∗ then P else Q where ∗ ∈ {!hvi, ?(x)} continues as the process Q. Rule (CALL) describes the evolution of a recursion process. The rules (EQUIV) and (DEQUIV) are used to rearrange a system in order to apply a rule. Rule (PAR) is used to compose larger systems from smaller ones by putting them in parallel, and considering the union of multisets of actions. The rules devoted to the passing of time are starting with letter D.
A computational step is captured by a derivation of the form:
N −→Λ N1 t N ′.
This means that a step is a parallel execution of individual actions of Λ followed by a time step.
Performing a step N −→Λ N1 t N ′ means that N ′ is directly reachable from N . If there is no applicable action (Λ = ∅), N −→Λ N1 t N ′ is written N t N ′ to indicate (only) the time progress.
Proposition 1 For any systems N , N ′ and N ′′, the following hold:
N t N ′′ and N ′′ t′ N ′.
1. If N t N ′ and N t N ′′, then N ′ ≡ N ′′;
2. N (t+t′) N ′ if and only if there is a N ′′ such that
The f rst item of Proposition 1 states that the passage
of time does not introduce any nondeterminism into
the execution of a process. Moreover, if a process is
able to evolve to a certain time t, then it must evolve
through every time moment before t; this ensures
that the process evolves continuously.
3. TRAVEL AGENCY EXAMPLE IN RTIMO
To illustrate the syntax and semantics of rTIMO ,
we use an example describing an understaffed
travel agency, presented also in
The f rst agent (i.e., process Agent1) leaves its home (i.e., the location homeAgent1) and goes to the central off ce of the agency (i.e., location office) in order to be assigned a certain local off ce for the current day (i.e., a location that will replace the location variable newloc). After arriving at the central off ce, it has to communicate with one of the executives on channel b after signing the attendance register, any time between 1 to 5 minutes (depending on l[[go[t1,t2]l′ then P ]] l[[go
′ ′ [max{0,t1−t },t2−t ] ′
l then P ]] ′ l⊲l l[[go[0,t]l′ then P ]] −−→ l′[[P ]]
′ {v/u}@l (COM) l[[a[0,t]!hvi then P else Q | a[0,t ]?(u) then P ′ else Q′]] −−−−−→ l[[P | {v/u}P ′]] (STOP) (DSTOP) (DMOVE) (MOVE0) (DPUT) (PUT0) (DGET) (GET0) (DCALL) (CALL) (DPAR) (PAR) (DEQUIV) (EQUIV) l[[a[t1,t2]!hvi then P else Q]] ′ ′ l[[a[max{0,t1−t },t2−t ]!hvi then P else Q]] l[[a[0,0]!hvi then P else Q]] −−−−−→ l[[Q]] l[[a[t1,t2]?(u) then P else Q]] ′ ′ l[[a[max{0,t1−t },t2−t ]?(u) then P else Q]] l[[a[0,0]?(u) then P else Q]] −−−−−→ l[[Q]] l[[{v/x}Pid]] l[[id(v)]]
′ l[[Pid]] t
l[[Pi′d]] id@l l[[{v/x}Pid]] −−−→ l[[Pi′d]]
id@l ′ l[[id(v)]] −−−→ l[[Pid]] where id(v) = Pid
def where id(v) = Pid
def λ l[[0]] 6−→
t l[[0]] l[[0]] the availability of one of the executives). Since the agent can use different means of transportations, and depending on the traff c, it can take between 5 to 10 minutes for the agent to reach the central off ce of the agency (this movement is described by the action go[5,10]office then P). The agent then moves to the given location (it can take between 3 to 5 minutes depending on the local off ce it has to reach) and advertises (over channel a) the f rst destination on the agency’s list (i.e., location dest1), in the form of a holiday pack for 100 monetary units.
Finally, after selling one travel package, the agent returns home (it can take between 5 to 8 minutes depending on the local off ce it departs from). The second and the third agent (i.e., processes Agent2 and Agent3) are similar to the f rst, but they have different homes (i.e., the locations homeAgent2 and homeAgent3), and advertise different destinations (i.e., locations dest2 and dest3), in the form of holiday packs for 200 and 300 monetary units, respectively.
Formally, we have: AgentX(homeAgentX : Loc) = AgentX(office : Loc) = b[1,5]?(newloc : Loc) go[5,10]office then AgentX(office : Loc) then (go[3,5] newloc else AgentX(office : Loc)
then AgentX(newloc : Loc)) AgentX(officei : Loc) = a[1,20]!hdestX, 100 · X i i then go[1,3] homeAgentX else go[1,3] homeAgentX then AgentX(homeAgentX : Loc) then AgentX(homeAgentX : Loc), where 1 ≤ i ≤ 6 and X ∈ {1, 2, 3} refers to the number of the agent.
The two executives (i.e., processes Executive1 and Executive2) reside at the central off ce (i.e., location office), and each chooses a local off ce (i.e., in a cyclic manner, from the locations office1, office3, office5, for process Executive1, and the locations office2, office4, office6 for process Executive2) that will be assigned to the next agent that comes to the central off ce (over channel b in a period of time between 1 and 5 time units for Executive1 and a period of time between 2 and 4 time units for Executive2, namely after each executive resolves some off ce paperwork that make different periods for the two executives). Formally, we have: Executive1(office1 : Loc) = b[1,5]!hoffice1i then Executive1(office3 : Loc) else Executive1(office1 : Loc) Executive1(office3 : Loc) =
b[1,5]!hoffice3i Executive1(office5 : Loc) = b[1,5]!hoffice5i then Executive1(office5 : Loc) else Executive1(office3 : Loc) then Executive1(office1 : Loc) else Executive1(office5 : Loc) Executive2(office2 : Loc) =
b[2,4]!hoffice2i Executive2(office4 : Loc) = b[2,4]!hoffice4i then Executive2(office4 : Loc) else Executive2(office2 : Loc) Executive2(office6 : Loc) = b[2,4]!hoffice6i then Executive2(office6 : Loc) else Executive2(office4 : Loc) then Executive2(office2 : Loc) else Executive2(office6 : Loc) The f rst customer (i.e., process Client1) leaves home (i.e., location homeC1) when he knows the agencies should be open and visits all of the three local off ces of the agency that are closest to his home (i.e., the locations office1, office2, and office3), in order, receives travel offers from the agents found at those local off ces, and chooses the cheapest travel destination. Then, he goes to the desired destination, spends a certain amount of time there, after which he returns home. The second customer (i.e., process Client2) has the same behaviour as the f rst, except that he has a different home (i.e., location homeClient2), the off ces closest to his home are locations office4, office5 and office6, and that he chooses the most expensive travel destination.
For simplicity, we consider that both clients have the same intervals of performing similar actions.
Formally, we have: Client1(homeClient1 : Loc) =
go[12,13] office1 Client1(office1 : Loc) =
then Client1(office1 : Loc) Client1(office2 : Loc) = a[0,4]?(destClient1,1 : Loc, costClient1,1 : N) 1 then (go[1,2] office2 else (go[1,2] office2 then Client1(office2 : Loc)) then Client1(office2 : Loc)) a[0,4]?(destClient1,2 : Loc, costClient1,2 : N) 2 then (go[1,3] office3 else (go[1,3] office3 then Client1(office3 : Loc)) then Client1(office3 : Loc)) Client1(office3 : Loc) = a[0,4]?(destlientC1,3 : Loc, costClient1,3 : N) 3 then (go[1,5] nextClient1 else (go[1,5] nextClient1 then Client1(nextClient1 : Loc)) then Clent1(nextClient1 : Loc)) Client1(destClient1,i : Loc) = go[1,5] homeClient1 then Client1(homeClient1 : Loc), for 1 ≤ i ≤ 3 where destClient1,i if costClient1,i = nextClient1 = homeClient1 minj∈{1,2,3}costClient1,j ∈ N otherwise.
Client2(homeClient2 : Loc) =
go[12,13] office4 Client2(office1 : Loc) =
then Client1(office4 : Loc) Client2(office5 : Loc) = Client2(office6 : Loc) = a[0,4]?(destClient2,1 : Loc, costClient2,1 : N) 4 then (go[1,2] office2 else (go[1,2] office2 then Client2(office5 : Loc)) then Client2(office5 : Loc)) a[0,4]?(destClient2,2 : Loc, costClient2,2 : N) 5 then (go[1,3] office6 else (go[1,3] office6 then Client2(office6 : Loc)) then Client2(office6 : Loc)) a[0,4]?(destClient2,3 : Loc, costClient2,3 : N) 6 then (go[1,5] nextClient2 else (go[1,5] nextClient2 then Client2(nextClient2 : Loc)) then Client2(nextClient2 : Loc)) Client2(destClient2,i : Loc) = go[1,5] homeClient2
then Client2(homeClient2 : Loc), for 1 ≤ i ≤ 3
where
destClient2,i if costClient2,i =
nextClient2 =
homeClient2
maxj∈{1,2,3}costClient2,j ∈ N
otherwise.
Towards a necessary automated verif cation of
complex distributed systems described by rTIMO ,
we provide f rst a relationship between rTIMO and
timed safety automata
Assume a f nite set of real-valued variables C ranged over by x, y, . . . standing for clocks, and a f nite alphabet Σ ranged over by a, b, . . . standing for actions. A clock constraint g is a conjunctive formula of constraints of the form x ∼ m or x − y ∼ m, for x, y ∈ C, ∼∈ {≤, <, =, >, ≥}, and m ∈ N. The set of clock constraints is denoted by B(C).
Definition 1 A timed safety automaton A is a tuple hN, n0, E, Ii, where • N is a f nite set of nodes; • n0 is the initial node; • E ⊆ N × B(C) × Σ × 2C × N is the set of edges; • I : N → B(C) assigns invariants to nodes. n −g−,a−,→r n′ is a shorthand notation for hn, g, a, r, n′i ∈ E. Node invariants are restricted to constraints of the form: x ≤ m or x < m where m ∈ N.
A network of timed automata is the parallel
composition A1 | . . . | An of a set of timed automata
A1, . . . , An combined into a single system using the
parallel composition operator and with all internal
actions hidden. Synchronous communication inside
the network is by handshake synchronisation of input
and output actions. In this case, the action alphabet
Σ consists of a? symbols (for input actions), a!
symbols (for output actions), and τ symbols (for
internal actions). A detailed example is found
in
A network can perform delay transitions (delay for some time), and action transitions (follow an enabled edge). An action transition is enabled if the clock assignment also satisf es all integer guards on the corresponding edges. In synchronisation transitions, the resets on the edge with an outputlabel are performed before the resets on the edge with an input-label. To model urgent synchronisation transitions that should be taken as soon as they are enabled (the system may not delay), a notion of urgent channels is used.
Let u, v, . . . denote clock assignments mapping C to non-negative reals R+. g |= u means that the clock values u satisfy the guard g. For d ∈ R+, the clock assignment mapping all x ∈ C to u(x) + d is denoted by u + d. Also, for r ⊆ C, the clock assignment mapping all clocks of r to 0 and agreeing with u for the other clocks in C\r is denoted by [r 7→ 0]u. Let ni stand for the ith element of a node vector n, and n[n′i/ni] for the vector n with ni being substituted ′ with ni.
A network state is a pair hn, ui, where n denotes a vector of current nodes of the network (one for each automaton), and u is a clock assignment storing the current values of all network clocks and integer variables.
Definition 2 The operational semantics of a timed automaton is a transition system where states are pairs hn, ui and transitions are def ned by the rules: • hn, ui −→d hn, u+di if u ∈ I(n) and (u+d) ∈ I(n), where I(n) = V I(ni); g,τ,r • hn, ui −→τ hn[n′i/ni], u′i if ni −−−→ n′i, g |= u,
u′ = [r 7→ 0]u and u′ ∈ I(n[n′i/ni]); • hn, ui −→τ hn[n′i/ni][n′j /nj ], u′i if there exist i 6= j such that 1. ni −g−i−,a−?−,r→i n′i, nj −g−j−,a−!,−r→j n′j , gi ∧ gj |= u, 2. u′ = [ri 7→ 0]([rj 7→
I(n[n′i/ni][n′j /nj]).
0]u) and u′ ∈ Building a timed automaton for each located process of rTIMO leads to the next result about the equivalence between an rTIMO network N and its corresponding timed automaton AN .
Theorem 1 Given an rTIMO network N with channels appearing only once in output actions, there exists a network AN of several parallel timed automata with a bisimilar behaviour.
A bisimilar behaviour is given by: • at the start of execution, all clocks in rTIMO and their corresponding timed automata are set to 0; • the consumption of a go action in a node l is
matched by a τ edge obtained by translation; • a communication rule is matched by a synchronization between the edges obtained by translations; • the passage of time is similar in both formalisms: in rTIMO the global clock is used to decrement by d all timers in the network when no action is possible, while in the timed automata all local clocks are decremented synchronously with the same value d.
Thus, the size of a timed safety automata AN is polynomial with respect to the size of a TIMO network N , and the state spaces have the same number of states. 5. MODELLING THE TRAVEL AGENCY EXAMPLE IN UPPAAL The model of the travel agency of Section 3 has three templates: • Agent(int dest) is the model of an agent with one integer parameter dest, as shown Graphically, a timed safety automata can be represented as a graph having a f nite set of nodes and a f nite set of labelled edges (representing transitions), using real-timed variables (representing the clocks of the system). The clocks are initialised with zero when the system starts, and then increased synchronously with the same rate. The behaviour of the automaton is restricted by using clock constraints, i.e. guards on edges, and local timing constraints called node invariants (e.g., see Figure 1). An automaton is allowed to stay in a node as long as the timing conditions of that node are satisf ed. A transition can be taken when the edge guards are satisf ed by clocks values. When a transition is taken, clocks may be reset to zero.
in Figure 2. Using the parameter dest we can initialize the three agents from Section 3 by creating the processes A1 = Agent(1), A2 = Agent(2) and A3 = Agent(3), where each agent sells a travel package to a different destination dest. It is also possible to instantiate any number of agents, or agents that sell the same travel package. • Executive(int o1, int o2, int o3) is the model of an executive with three integer parameters o1, o2 and o3, shown in Figure 2. The three parameters are used to initiate the two executives described in Section 3 by creating the processes E1 = Executive(1, 3, 5) and E2 = Executive(2, 4, 6), where each executive is given the off ce locations that he/she can assign to agents. As for the agents, it is possible to create more executives than the ones presented in Section 3. • Client(int id, int o1, int o2, int o3) is the model of a client with four parameters, shown in Figure 3. The parameters are used to initiate the two clients of Section 3 by creating the processes C1 = Client(1, 1, 2, 3) and C2 = Client(2, 4, 5, 6). The id parameter is used to uniquely identify a client, while the other parameters are used to identify three local off ces each client is allowed to visit before making a travel decision. As for Agent and Executive, any number of clients can be created.
system A1, A2, A3, E1, E2, C1, C2.
We explain in detail the Agent template of Figure 2 (the others are constructed in a similar manner). It has f ve locations: home, office, office b, office o and office a. The initial location is home, which corresponds to the fact that an agent is at home. The location has the invariant x <= 10 (taken from the rTIMO action go[5,10]) which has the effect that the location must be left within 10 time units. The outgoing transition towards location office is guarded by the constraints 5 <= x and x <= 10, which correspond to the above mentioned go rTIMO action. Once at location office, the agent can either synchronize on channel b[o] with an executive or, if the channel expires, create another instance in order to be able to receive an off ce location from an executive. After the communication is performed, the agent is at location office b (meaning that it successfully received the location newloc = o of the off ce he is detached to), and is ready to move to the assigned location officeo. After arriving at officeo, he awaits for a client for at most 20 time units, to which he must communicate the travel package on channel a[newloc][dest]!. Regardless of the fact that he interacts with a client or not, he moves within 20 time units to the location office b where he is ready to go home in order to prepare for a new working day. Thus, an agent has a cyclic evolution (a similar behaviour as one of the executives and of the clients). 6. VERIFYING PROPERTIES OF TRAVEL AGENCY BY USING UPPAAL According to the results and descriptions presented in the previous section, we can verify time bounded distributed systems with mobility presented as rTIMO networks by using UPPAAL. UPPAAL can be used to check temporal properties of networks of timed automata, properties expressed in Computation Tree Logic (CTL). If φ and ψ are boolean expressions over predicates on nodes, integer variables and clock constraints, then the formulas have the following forms: A [ ] φ - Invariantly φ; A h i φ - Always Eventually φ;
φ ψ - φ always leads to ψ. This is a shorthand for A [ ] (φ ⇒ A h i ψ) The formulas can be of two types: path formulae (quantify over paths or traces of the model) and state formulae (individual states). Path formulae can be classif ed into reachability (E h i φ), safety (A [ ] φ and E [ ] φ) and liveness (A h i φ and φ ψ). Reachability properties are used to check whether there exist a path starting at the initial state, such that φ is eventually satisf ed along that path. Safety properties are used to verify that something bad will never happen, while liveness properties check whether something will eventually happen. We present various properties that could be analyzed and verif ed for our example from Section 3. We have used an Intel PC with 8 GB memory, 2.50 GHz × 4 CPU and 64-bit Ubuntu 14.04 LTS to run the experiments. The results are presented for each analyzed property.
Example 1 Given the uncertainty of the delay in migration and communication, the size of the potential interactions in rTIMO systems grows exponential making the software verif cation a necessity. We use UPPAAL to perform this kind of verif cations for the travel agency example presented in Section 3, for both safety and liveness properties. Here we present only some of the formulas/properties verif ed by using UPPAAL.
The formulae C1.office1 C1.home, shorthand for A[ ](C1.office1 ⇒ Ah iC1.home, describe that, once the client C1 is in the office1 location, then it will always reach the home location. This implies that after leaving location office1, even whether the client visits or not the locations office2 and office3, the client C1 goes to the desired location, after which returns home. • Eh i C1.home imply C1.dest1
This formulae is used to check whether once the client C1 is in the home location, then it possibly reaches the dest1 location. This implies that if the client C1 leaves the home location, one of its travels takes him to location dest1. In a similar manner it can be checked that there are evolutions in which the client C1 visits one of the locations dest2 or dest3. • Eh i A1.office and A2.office and A3.office This is checking whether or not the agents A1, A2 and A3 reach the office location at the same time. Due to the uncertainty of the delay in migration and communication and of the fact that each agent has different timing constraints, having all agents at location office may not happen in all the possible evolutions.
This is checking that there exists no deadlock. This implies that, whatever are the interactions between the involved participants, the evolution never stops. This means that after a working day the agents go the next day to work, while the clients continue to look for travel packages in the following days.
For this property, we have stopped the verif cation process after 57609 seconds due to the fact that the RAM was fully used (as it can be seen below).
Since the verif cation of the previous property
was stopped due to insuff cient RAM, we try a
similar verif cation of “no deadlock” for smaller
systems. For systems with a smaller number
of agents, executives and clients the “no
deadlock” property is satisf ed. For one agent,
one executive and one client the UPPAAL
verif cation returned:
Adding another agent takes more time to verify,
but the property still holds:
Several other properties of rTIMO systems can be
verif ed by using UPPAAL .
7. CONCLUSION AND RELATED WORK
In this paper we presented time bounded extension
of rTIMO , suitable to work in complex distributed
systems with mobility. It is different from all
previous approaches since it encompasses specif c
features as real-time timeouts given as intervals,
explicit locations, time bounded migration and
communication. The parallel execution of a step is
provided by multiset labelled transitions. We have
presented an example of applying rTIMO to an
understaffed travel agency, illustrating that rTIMO
provides an appropriate framework for modelling and
reasoning about time bounded distributed systems
with migration and interaction/communication. We
have shown that we can model and verify
realtime systems (e.g., the travel agency) corresponding
to rTIMO networks by using UPPAAL . As rTIMO is
a prototype language, a f exible representation of
a travel agency is given as a number of parallel
processes that are instances of the AX, EX and
CX. The implementation of rTIMO processes in
UPPAAL is natural due to the fact that in UPPAAL it is
possible to use templates. For the running example
this allows, by proper instantiations, to create any
number of agents, executives and clients that can
interact when placed in parallel. It is easy to note
that the formalism presented in
Several proposals of process calculi for real-time
modelling and verif cation have been presented in
the literature: timed CSP
Acknowledgements. Many thanks to the reviewers for their useful comments. The work was supported by a grant of the Romanian National Authority for Scientif c Research, project number PN-II-ID-PCE2011-3-0919.