Formal Methods for Specification and Verification of
Ad hoc Network Protocols

Home page
Contact us








Research Description

The high and ever-growing complexity, as well as our great dependency on today's dynamic and often safety-critical computing systems, renders the need of scientific methodologies for the development of reliable algorithmic solutions for these computational environments widely acknowledged. This project deals with this challenge and aims to investigates the foundations of the modelling, development and analysis of ad hoc networks. Specifically its objectives are summarized below:

- A first to-date comprehensive study of formal methods for the analysis of ad hoc network protocols.

- An in-depth and comprehensive evaluation of ad hoc networks with emphasis on their main characteristics, problems arising therein and the parameters that affect their behavior.

- Correctness analysis of a number of ad-hoc network protocols using process algebras and I/O automata.

- Evaluation of each of the two frameworks with respect to their applicability for the task at hand and the first practical comparison (based on specific case studies) between process algebras and I/O automata for system specification and analysis.

- Proposal of specialized, improved methodologies and techniques for formally specifying and rigorously verifying the correctness of ad hoc networked systems.