Analysing AWN-specifications using mCRL2

Rob van Glabbeek, Peter Höfner and Djurre van der Wal

Abstract: We develop and implement a translation from the process Algebra for Wireless Networks (AWN) into the milli Common Representation Language (mCRL2). As a consequence of the translation, the sophisticated toolset of mCRL2 is now available for AWN-specifications. We show that the relation linking AWN-specifications with their translations is a strong bisimulation; hence all safety properties can be automatically checked using the toolset. To show usability of our translation we report on a case study.


This page contains complimentary data concerning a submitted paper. In particular it provides a document containing a (full) proof showing that our translation function establishes a strong bisimulation. It further provides a self-contained jar-file for our implementation.
This webpage is temporary: as soon as the work is finished the results will be moved to more permanent locations.


The Proof

In our submitted paper, which can be found here, we sketch a proof. The full proof can be found here. Please note that the report containing the full proof is a draft only; although the proof is finished, it still lacks explanations, related work, etc.
When the report is finished it will be published at arXive, or somewhere similar.


The Implementation

Our research reports on the implementation of a property-preserving translation from AWN-specification into mCRL2. Currently, we provide a stand-alone jar-file of our implementation. This archive inlcudes the two applications we reported on: the AWN-specifications for the leader-election protocol as well as the AODV routing protocol can also be downloaded separately.
The implementation will be made available at github, or something similar,


Contact

Peter Höfner: peter.hoefner <at> data61.csiro.au