Informatisches Kolloquium Sommersemester 2008

Montag, 19. Mai 2008

Lars M. Kristensen,
Associate Professor, Department of Computer Science,
University of Aarhus, Denmark

Let's aim at going all the way — from Formal Specification and Verification to Implementation of Communication Protocols

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 use of formal modelling and state space exploration (model checking) is a main approach to model-based development and verification of protocols. 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.

Many projects have been carried out and reported in the literature on successful application of formal modelling and verification of Internet protocols. The formal models are, however, seldom used (directly) as a basis for implementation of the protocols.

This talk presents our initial work conducted in the ASCoVeCo research project concerned with formal modelling, verification, and implementation of the Dynamic MANET On-demand Routing (DYMO). DYMO is a routing protocol currently being developed by the IETF MANET working group for multi-hop communication in mobile ad-hoc networks (MANETs). A formal model of the DYMO protocol has been developed using the Coloured Petri Nets (CPNs) modelling language and is being verified using state space exploration.

As part of the project, we have developed ASAP which is an Eclipse-based computer tool for state space exploration of CPN models, and the Virtual Internetworking Environment (VINE) to be used as the initial target platform for the DYMO implementation.

Kontakt

Dr. Daniel Moldt
Telefon 2447