The ASCoVeCo project: Exploring Large State Spaces

Abstract:

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 protocol under 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 development of 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 http://www.daimi.au.dk/~ascoveco