Formal Methods for Specification and Verification of
Ad hoc Network Protocols

Home page
Contact us








This research (called PROODOS) investigates the foundations of the modelling, development and analysis of dynamic systems. A dynamic system is a system with a dynamically-evolving interconnection composed of a changing number of components which can be created and destroyed as computation proceeds. The dynamic behaviour of these systems makes their understanding and development a challenging task. Thus, despite their wide use the need to create scientific methodologies for these complicated and continuously-evolving environments is widely recognized.

PROODOS tackle this challenge by investigating the specification and verification of a class of dynamic systems, that of ad hoc networks , and aims to propose methodologies for the development of correct, efficient and reliable solutions to problems originating in them. During this research the frameworks of Process Algebra and I/O Automata. are employed to model and analyze algorithms in ad hoc networks which eventually enable the evaluation of the two methodologies according to their applicability for the field under study.