Thesis Topic Details

Topic ID:
3504
Title:
Timed Process Algebra for Wireless Mesh Networks
Supervisor:
Peter Hofner
Research Area:
Formal Methods
Associated Staff
Assessor:
Rob van Glabbeek
Topic Details
Status:
Active
Type:
Research
Programs:
CS
Group Suitable:
No
Industrial:
No
Pre-requisites:
interest in applying Formal Methods and logic-based calculi in general; previous knowledge about process algebra is appreciated, but not necessary
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 performance of current systems often does 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 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.

Classical routing protocol specifications are usually written in plain English. Often this yields ambiguities, inaccuracies or even contradictions. The use of Formal Methods like process algebra avoids these problems and leads to a precise description of protocols. Among others we have modelled one of the standard protocols using process algebra, namely AODV.
After setting up an unambiguous specification, we were able to verify key properties, such as loop freedom.

However, so far we have abstracted from all aspects of timing.
This project aims at extending our specification with time, and proving key properties for the timed variant of the protocol.
Time permitting, we would also want to analyse other routing protocols where time plays a greater role.
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.