=Paper=
{{Paper
|id=Vol-1431/paper8
|storemode=property
|title=Timeout Interaction and Migration in Distributed Systems
|pdfUrl=https://ceur-ws.org/Vol-1431/paper8.pdf
|volume=Vol-1431
|dblpUrl=https://dblp.org/rec/conf/vecos/Ciobanu15
}}
==Timeout Interaction and Migration in Distributed Systems==
https://ceur-ws.org/Vol-1431/paper8.pdf
Timeout Interaction and Migration
in Distributed Systems
Gabriel Ciobanu
Romanian Academy, Institute of Computer Science, Iaşi, Romania
gabriel@info.uaic.ro
The complexity of distributed systems is increasing, action does not happen before this deadline, the
and so they require appropriate formalisms and process gives up and switches its operation to an
techniques for their specificatio and verification alternative process. E.g., a timer ∆5 associated to
Since these distributed systems grow more complex an output action a∆5 !hvi makes the channel available
and more powerful, it is important to fin scaling for communication only for a period of 5 time units.
formal methods for both specificatio and verifi Considering suitable data sets including a set Loc
cation. Successful formalisms for specificatio and of locations, a set Chan of communication channels
verificatio of certain distributed systems are given and a set Id of process identifier , the syntax of
by networks of timed automata and by Petri nets; T I M O is presented in Table 1.
however, these formalisms are not easily scalable,
a reason why we look for compositional specificatio Using T I M O , we can specify and analyse complex
and verificatio techniques. In terms of specification timing systems in a new and intuitive way. Aiming
a process calculus would solve the compositional to bridge the gap between the existing theoretical
issue. Moreover, in distributed systems coordination approach of process calculi and forthcoming realistic
is given by time scheduling, access to resources, programming languages for distributed systems,
and interaction among processes. When modelling T I M O represents in several aspects a prototyping
distributed systems it is useful to have an explicit language for multi-agent systems featuring mobility
notion of location, local clocks, explicit migration and and local interaction. Starting with a firs version
resource management. proposed in Ciobanu and Koutny (2008), several
variants were developed during the last years. We
We have introduced in Ciobanu and Koutny (2008) mention here the access permissions given by a type
a rather simple and expressive formalism called system in perT I M O Ciobanu and Koutny (2011a),
T I M O as a simplifie version of timed distributed as well as a probabilistic extension pT I M O Ciobanu
π-calculus Ciobanu and Prisacariu (2006) which and Rotaru (2013). Inspired by T I M O , a fl xible
is an extension of distributed π-calculus Hennessy software platform was introduced in Ciobanu and
(2007). T I M O is a process calculus with explicit Juravle (2009, 2012) to support the specificatio
migration allowing the use of timers for controlling of agents allowing timed migration in a distributed
process mobility and interaction. Migration involves environment.
several explicit locations. Each location has a local
clock, modelling distributed systems in a more In terms of verification interesting properties de-
accurate way. Timing constraints for migration allow scribed by T I M O regarding could be analysed and
to specify a temporal timeout after which a process checked. The properties of distributed systems de-
must move to another location. Two processes may scribed by T I M O refer to process migration, time con-
communicate only if they are present at the same straints, bounded liveness and optimal reachability
location. A timer denoted by ∆3 associated to a Aman et. all (2012); Ciobanu and Koutny (2011b).
migration action go∆3 work indicates that the process A verificatio tool called T I M O@PAT Ciobanu and
moves to location work after at most 3 time units. Zheng (2013) was developed by using Process
It is also possible to indicate a deadline for a Analysis Toolkit (PAT), an extensible platform for
communication over a channel; if a communication model checkers. A formal relationship between
P ::= a∆lt !h~v i then P else P ′ p (output)
a∆lt ?(~u:X)~ then P else P ′ p (input)
go ∆lt
l then P p (move)
P | P′ p (parallel)
0p (termination)
id(~v ) (definition
sP (stalling)
L ::= l[[P ]] Located Processes
N ::= L p L|N Networks
Table 1: T I M O Syntax.
rT I M O and timed automata presented in Aman and Ciobanu, G. and Koutny, M. (2008) Modelling and
Ciobanu (2013) allows the use of model checking Verificatio of Timed Interaction and Migration.
capabilities provided by the well-known verificatio In Fiadeiro, J.L., Inverardi, P. (Eds.) FASE 2008,
tool U PPAAL . A probabilistic temporal logic called Lecture Notes in Computer Science 4961, 215–
PLTM was introduced in Ciobanu and Rotaru (2013) 229.
to verify complex probabilistic properties making
explicit reference to specifi locations, temporal con- Ciobanu, G. and Koutny, M. (2011) Timed Migration
straints over local clocks and multisets of actions. and Interaction With Access Permissions. In
Butler, M., Schulte, W. (eds.) FM 2011, Lecture
Notes in Computer Science 6664, 293–307.
Acknowledgements. The work was supported by
a grant of the Romanian National Authority for Ciobanu, G. and Koutny, M. (2011) Timed Mobility
Scientifi Research, project PN-II-ID-PCE-2011-3- in Process Algebra and Petri nets. The Journal of
0919. Logic and Algebraic Programming 80(7), 377–391.
Ciobanu, G. and Prisacariu, C. (2006) Timers for
REFERENCES Distributed Systems. In Di Pierro, A. and Wiklicky,
H. (Eds.) QAPL 2006,Electronic Notes in Theoretic
Aman, B. and Ciobanu, G. (2013) Real-Time Computer Science 164(3), 81–99.
Migration Properties of rT I M O Verifie in U PPAAL .
In Hierons, R., Merayo, M.and Bravetti, M. (Eds.), Ciobanu, G. and Rotaru, A. (2013) A Probabilistic
SEFM 2013. Lecture Notes in Computer Science Logic for P T I M O. In Liu, Z., Woodcock, J. and Zhu,
8137, 31–45. H. (Eds.) ICTAC 2013, Lecture Notes in Computer
Science 8049, 141–158.
Aman, B., Ciobanu, G. and Koutny, M. (2012) Be-
havioural Equivalences over Migrating Processes Ciobanu, G. and Zheng, M. (2013) Automatic
with Timers. In Giese, H. and Rosu, G. (Eds.) Analysis of T I M O Systems in PAT. In Proc.
FMOODS/FORTE 2012, Lecture Notes in Com- 18th International Conference on Engineering of
puter Science 7273, 52–66. Complex Computer Systems (ICECCS 2013),
IEEE Computer Society, 121–124.
Ciobanu, G. (2008) Behaviour Equivalences in
Timed Distributed π-Calculus. In Wirsing, M., Hennessy, M. (2007) A distributed π-calculus.
Banâtre, J.-P., Hölzl, M. and Rauschmayer, A. Cambridge University Press.
(Eds.), Lecture Notes in Computer Science 5380,
190–208.
Ciobanu, G. and Juravle, C. (2009) A Software
Platform for Timed Mobility and Timed Interaction.
In Lee, D., Lopes, A. and Poetzsch-Heffter, A.
(Eds.) FMOODS/FORTE 2009, Lecture Notes in
Computer Science 5522, 106–121.
Ciobanu, G. and Juravle, C. (2012) Flexible
Software Architecture and Language for Mobile
Agents. Concurrency and Computation: Practice
and Experience24, 559–571.