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.