INVESTIGADORES
BRABERMAN Victor Adrian
congresos y reuniones científicas
Título:
An Architecture-centric approach to the development of a distributed model-checker for time automata
Autor/es:
FERNANDO SCHAPACHNIK; VÍCTOR BRABERMAN; ALFREDO OLIVERO
Lugar:
Orlando, EEUU
Reunión:
Conferencia; Poster Session International Conference on Software Engineering; 2002
Resumen:
Research in Model-Checking is focused on increasing the size
of the problems tools can deal with. The ultimate wave has
been the use of Distributed-Computing, where a cluster of
computers work together to solve the problem [8, 3, 9].
In our work we present a distributed model-checker that
evolves from the tool Kronos [5] and can handle backwards
computation of TCTL-reachability formulae [1] over timedautomata
[2]. Our proposal, including the arguments of its
correctness, is based on software architectures, using a notation
adapted from [6]. We find such an approach a natural
and general way to address the development of complex tools
that need to incorporate new features and optimizations as
they evolve.
We introduce some interesting features such as a priori
[2]. Our proposal, including the arguments of its
correctness, is based on software architectures, using a notation
adapted from [6]. We find such an approach a natural
and general way to address the development of complex tools
that need to incorporate new features and optimizations as
they evolve.
We introduce some interesting features such as a priori
automata
[2]. Our proposal, including the arguments of its
correctness, is based on software architectures, using a notation
adapted from [6]. We find such an approach a natural
and general way to address the development of complex tools
that need to incorporate new features and optimizations as
they evolve.
We introduce some interesting features such as a prioria priori
graph partitioning (using METIS [7], a standard library for
graph partitioning), a sophisticated machinery to reach optimum
performance (communication piggybacking and delayed
messaging) and dead-time utilization, where every processor
uses time intervals of inactivity to perform auxiliary,
time-consuming tasks that will later speed up the rest of the
computation.
The correctness proof strategy combines an architecture
evolution with the theoretical results about fix point calculation
developed by Patrick Cousot in 1978 [4].