Thesis Topic Details

Topic ID:
3485
Title:
Model Checking Tool Suite for Protocol Development
Supervisor:
Peter Hofner
Research Area:
Software Engineering, Formal Methods
Associated Staff
Assessor:
Rob van Glabbeek
Topic Details
Status:
Active
Type:
Research
Programs:
CS SE
Group Suitable:
No
Industrial:
No
Pre-requisites:
Experience in Java, knowledge about model checking and mesh networks is not required
Description:
Wireless Mesh Networks (WMNs) are a promising technology that is currently being used in a wide range of application areas, including Public Safety, Transportation, Mining, etc. Typically, these networks do not have a central component (router), but each node in the network acts as an independent router, regardless of whether it is connected to another node or not. They allow reconfiguration around broken or blocked paths by ``hopping'' from node to node until the destination is reached. Unfortunately, the current systems often do not live up to the expectations of end users in terms of performance and reliability, as well as ease of deployment and management. We explore and develop new adaptive network protocols and mechanisms for Wireless Mesh Networks that can overcome the major performance and reliability limitations of current systems. To support the development of these new protocols, the project also aims at new Formal Methods based techniques, which can provide powerful new tools for the design and evaluation of protocols and can provide critical assurance about protocol correctness and performance. Close collaboration with industry partners ensures the use-inspired nature of the project.

The techniques used for modelling, analysing and verifying routing protocols for WMNs are based on a simple programming language, which offers expressions for (arbitrary) data structures and basic primitives for WMNs, such as broadcast and unicast. The intention is to use this language right from the beginning when designing protocols; but this can only be achieved if
tools support the development.

In the past a translator from the specification language to the input language of the model checker Uppaal has been developed.
Moreover a text-editor front-end for the specification language has been developed.
The first task of the project is the combination of the two projects; by this a tool suite is created which can be used to
design new protocols and which immediately offers model checking support.
The second (major) aim is to extend the tool suite by a set of standard tests which can be used to automatically analyse protocols during development
and to offer on-the-fly feedback to the user.
Comments:
--
Past Student Reports
 
No Reports Available. Contact the supervisor for more information.

Check out all available reports in the CSE Thesis Report Library.

NOTE: only current CSE students can login to view and select reports to download.