2007.06.04

The ASCoVeCo project: Exploring Large State Spaces

Communication protocols play a still more important role in our everyday use
of information technology, and it is therefore of vital importance that they
work as intended. Protocols are, however, challenging to design and
implement. Important reasons for this are the inherent presence of
concurrency and non-determinism which induces complex behaviour thereby
making testing and debugging difficult. The ASCoVeCo research project
(2006-2009) is concerned with model-based verification of protocols using
state space exploration. The basic idea of state space exploration is to
verify behavioural properties of protocols by exploring the reachable states
and state changes of the protocolunder consideration. A main challenge in
applying the approach in practice is the size of the explored state space.

In this talk we present selected examples of the work conducted in the
ASCoVeCo project which includes developmentof algorithms and
data-structures for handling large state spaces, development of ASAP which
is an Eclipse-based computer tool for state space exploration, and practical
application of the developed methods and computer tools on protocols for
mobile networks.

For further information on the ASCoVeCo project, see
www.daimi.au.dk/~ascoveco