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: Ansgar Fehnker ,
Peter Höfner ,
Rob van Glabbeek
end: July 2018
type: 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.