• Homepage
• Publications
• ASAP
• Download
• People

The ASCoVeCo Project
Dept. of Computer Science
University of Aarhus
Email:

DAIMI / Projects / ASCoVeCo

The ASCoVeCO project:

Advanced State Space Methods and Computer tools for Verification of Communication Protocols

The increasing use of laptops, handheld computers, mobile phones and the Internet means that data communication directly and indirectly plays a significant role in the everyday life of most people. Communication protocols are the key building blocks that make data communication possible since they define the components, rules, and languages that enable data communication. As a consequence, it is of vital importance that the protocols work as intended, e.g., that they do not contain errors that can result in system malfunctions and crashes.

The project is concerned with model-based verification of communication protocols using state space methods. The basic idea underlying state space methods is to compute all reachable states and state changes of the protocol and to represent these as a directed graph where the nodes represent states and arcs represent occurring events. State spaces can be constructed fully automatically and from a constructed state space it is possible to answer a large set of verification questions concerning the behavior of a protocol using model checking techniques.

The project has the following four main research objectives and is expected to contribute to the increased application of formal models and verification for the development of protocols:

• Development of new state space methods for computer-aided reasoning about protocols.
• Development of advanced algorithms and data-structures providing the foundation for making space and time efficient implementations of state space methods in computer tools.
• Implementation of prototypes of computer tools supporting the developed state space methods, and determining how the developed state space methods are most efficiently implemented in practice.
• Industrial case studies evaluating the developed state space methods and supporting state space tool prototypes in practice on protocols.

The project was initiated via a project grant (September 2006 - January 2010) from the Danish Research Council for Technology and Production Sciences.