Djurre van der Wal - Verification of Wireless Network Protocols (AWN)

author:Djurre van der Wal
title:Verification of Wireless Network Protocols (AWN)
company:Data61, Australia (formerly NICTA)
keywords:AWN, mCRL2, model transformation, verification
topics:Case studies and Applications, Languages
committee:prof.dr. J.C. van de Pol
dr. A. Fehnker
Peter Höfner
Rob van Glabbeek

MTV master project


Model checking a process algebra for wireless mesh networks with a formally validated mCRL2 back end

AWN (Algebra for Wireless Network protocols) is a process algebra that has been developed as a contribution to the formalization of wireless network protocols. One of the ambitions for AWN is that it will be possible to automatically modeland verify AWN specifications with existing model checking toolsets via translations of AWN to input that these toolsets accept.

My graduation project specifically involves the development of a translation from AWN to mCRL2 and to formally determine to which extent this translation is valid so that future users can be confident about the relation between their input and the results that mCRL2 produces. It is expected that this relation can be developed to be a strong bisimulation relation.