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 translation respects strong bisimilarity; hence all safety properties can be automatically checked using the toolset. To show usability of our translation we report on a case study.
Paper: pdf
This page contains complimentary data concerning the paper mentioned above. 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.
In our paper 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 arXiv, or somewhere similar.
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 <at> hoefner-online.de
Last update: Sep. 01, 2018