Romanian Academy, Institute of Computer Science, Iasi
TiMo in Timisoara
In complex distributed systems, coordination is given by time scheduling, access to resources, and interaction among processes. When modelling distributed systems it is useful to have an explicit notion of location, local clocks, explicit migration and resource management.
A rather simple and expressive formalism called TiMo was introduced in 2008 by G.Ciobanu and M.Koutny as a simplified version of timed distributed pi-calculus. It aims to bridge the gap between the existing (theoretical) process calculi and forthcoming realistic languages for multi-agent systems. Several variants were developed during the last years: a probabilistic extension pTiMo, a real-time version rTiMo, access permissions given by a type system in perTiMo. Inspired by TiMo, a
flexible software platform was introduced to support the specification of agents allowing timed migration in a distributed environment.
Interesting properties of distributed systems described by TiMo refer to process migration, time constraints, bounded liveness and optimal reachability. A verification tool called TiMo@PAT was developed by using Process Analysis Toolkit (PAT), an extensible platform for model checkers.
A formal relationship between rTiMo and timed automata allows the use of model checking capabilities provided by UPPAAL. A probabilistic temporal logic called PLTM was introduced to verify properties making explicit reference to specific locations, temporal constraints over local clocks
and multisets of actions.
More information on TiMo family is available at
Gabriel Ciobanu is a Researcher at the Romanian Academy of Sciences (Institute of Computer Science), and a Professor at “A.I.Cuza” University of Iasi. His interests include Distributed Systems and Concurrency, Biologically Inspired Formalisms (membrane computing), and Theory of
Programming (semantics, formal methods, process calculi). Gabriel Ciobanu has served on the programme committees of numerous international conferences, and edited several books on these topics. For his research, he received two Awards of the Romanian Academy of Sciences. He is the
Editor-in-Chief of Scientific Annals of Computer Science (http://www.info.uaic.ro/