-
We have introduced in
Ciobanu and Koutny (2008)
a rather simple and expressive formalism called
TIMO as a simplifie version of timed distributed
π-calculus
Ciobanu and Prisacariu (2006)
which
is an extension of distributed π-calculus Hennessy
(2007). TIMO is a process calculus with explicit
migration allowing the use of timers for controlling
process mobility and interaction. Migration involves
several explicit locations. Each location has a local
clock, modelling distributed systems in a more
accurate way. Timing constraints for migration allow
to specify a temporal timeout after which a process
must move to another location. Two processes may
communicate only if they are present at the same
location. A timer denoted by Δ3 associated to a
migration action goΔ3work indicates that the process
moves to location work after at most 3 time units.
It is also possible to indicate a deadline for a
communication over a channel; if a communication
action does not happen before this deadline, the
process gives up and switches its operation to an
alternative process. E.g., a timer Δ5 associated to
an output action aΔ5!hvi makes the channel available
for communication only for a period of 5 time units.
Considering suitable data sets including a set Loc
of locations, a set Chan of communication channels
and a set Id of process identifier , the syntax of
TIMO is presented in Table 1.
Using TIMO , we can specify and analyse complex
timing systems in a new and intuitive way. Aiming
to bridge the gap between the existing theoretical
approach of process calculi and forthcoming realistic
programming languages for distributed systems,
TIMO represents in several aspects a prototyping
language for multi-agent systems featuring mobility
and local interaction. Starting with a firs version
proposed in
Ciobanu and Koutny (2008)
, several
variants were developed during the last years. We
mention here the access permissions given by a type
system in perTIMO
Ciobanu and Koutny (2011
a),
as well as a probabilistic extension pTIMO
Ciobanu
and Rotaru (2013)
. Inspired by TIMO , a fl xible
software platform was introduced in
Ciobanu and
Juravle (2009
, 2012) to support the specificatio
of agents allowing timed migration in a distributed
environment.
In terms of verification interesting properties
described by TIMO regarding could be analysed and
checked. The properties of distributed systems
described by TIMO refer to process migration, time
constraints, bounded liveness and optimal reachability
Aman et. all (2012
);
Ciobanu and Koutny (2011
b).
A verificatio tool called TIMO@PAT
Ciobanu and
Zheng (2013)
was developed by using Process
Analysis Toolkit (PAT), an extensible platform for
model checkers. A formal relationship between
aΔlt ?(~u:X~ ) then P else P ′ p
goΔlt l then P p
P | P ′ p
0 p
id(~v)
sP
L ::= l[[P ]]
N ::=
L p L | N
(input)
(parallel)
(definition
rTIMO and timed automata presented in
Aman and
Ciobanu (2013)
allows the use of model checking
capabilities provided by the well-known verificatio
tool UPPAAL . A probabilistic temporal logic called
PLTM was introduced in
Ciobanu and Rotaru (2013)
to verify complex probabilistic properties making
explicit reference to specifi locations, temporal
constraints over local clocks and multisets of actions.
Acknowledgements. The work was supported by
a grant of the Romanian National Authority for
Scientifi Research, project
PN-II-ID-PCE-2011-30919.
Hennessy, M. (2007) A distributed π-calculus.
Cambridge University Press.