Dynamic Networks of Timed Automata for Collaborative Systems: a Network
Monitoring Case Study
Salvatore Campana
s.campana@computervaritt.it
Computer VAR ITT - Verona, Italy
Luca Spalazzi
spalazzi@univpm.it
DIIGA, Universita` Politecnica delle Marche - Ancona, Italy
Francesco Spegni
spegni@diiga.univpm.it
DIIGA, Universita` Politecnica delle Marche - Ancona, Italy
Abstract
We introduce Dynamic Networks of Timed Automata, an
extension of (Networks of) Timed Automata[7, 22] useful
for specifying concurrently executing timed-processes. The
main difference with Timed Automata is that we allow the
instantiation at run-time of multiple copies of automata. In
this paper we also show an industrial case study where a
system for monitoring a network of wireless devices is built
applying Dynamic Networks of Timed Automata. The net-
work is characterized by a high degree of dynamism, since
its infrastructure is fixed but a big amount of its hosts con-
tinuously connect and disconnect. We see how extending
XAL, [13] an executable language for Timed Automata, we
can first model our system, made of cooperating timed pro-
cesses, and finally transform such model into an executable
application. We also show how to model-check some prop-
erties which are relevant for our application, expressing
them through a temporal logic called TCTL and using ex-
isting formal methods and tools.
1. Introduction
A collaborative system is given by a multitude of agents
that cooperate in order to reach a common goal. Such agents
are usually humans or automated, perhaps software, proce-
dures, and are generally characterized by the necessity to
interact for reaching their aims. In this paper we mainly
focused on the latters.
Here we introduce Dynamic Networks of Timed Au-
tomata (DNTA), a formalism that extends (Networks of)
Timed Automata (NTA) [7, 22]. The added value that we
give is the possibility to describe a timed-system where
automata (and thus processes) can be instantiated and de-
stroyed at run-time. This brings a whole new flexibility to
the language, very useful for describing processes that are
intrinsecally dynamical, for which the programmer cannot
foresee how many copies of a single process is needed to
accomplish the computation.
Together with it, we integrate DNTA in XAL [13], an
executable language that allows to describe an application
as one or more cooperating automata with temporal con-
straints. In [13], it has been shown how to use XAL in
order to formalize and contemporary implement precise
SLAs (Service Level Agreements) specifications in real-
world web-applications and services.
From a Software Engineering point of view we think that
XAL represents a good balance between a formal model, i.e.
a theoretical description of the process behavior on which
you can reason, and a programming language, through
which the software engineer can write her/his applications.
We chose to define DNTA, and then XAL, extending Net-
works of Timed Automata because the latter has a well de-
fined semantics and because it has well known verification
procedures, mainly based on bisimulation [7] and model-
checking [22, 33, 9].
In our approach we distinguish between automaton defi-
nition and automaton instance. A system is defined as a set
of automaton definitions while its execution is described by
a set of automaton instances that varies over the time. This
is very close in principle to the difference between what is
often kwown as Class and Instance for usual object-oriented
languages. From a collaborative system point of view, the
proposed language allows us to model complex systems
where several components are created or destroyed at run-
time, and cooperate each others exchanging messages.
We underline how, allowing to split complex tasks into
smaller subtasks that collaborate together, we give the pos-
sibility to lower the complexity of the components of the
overall system and we give the opportunity to later re-use
the definition of a process. To understand how this helps