# Mechanization of the Algebra for Wireless Networks (AWN)

 Title: Mechanization of the Algebra for Wireless Networks (AWN) Author: Timothy Bourke Submission date: 2014-03-08 Abstract: AWN is a process algebra developed for modelling and analysing protocols for Mobile Ad hoc Networks (MANETs) and Wireless Mesh Networks (WMNs). AWN models comprise five distinct layers: sequential processes, local parallel compositions, nodes, partial networks, and complete networks. This development mechanises the original operational semantics of AWN and introduces a variant 'open' operational semantics that enables the compositional statement and proof of invariants across distinct network nodes. It supports labels (for weakening invariants) and (abstract) data state manipulations. A framework for compositional invariant proofs is developed, including a tactic (inv_cterms) for inductive invariant proofs of sequential processes, lifting rules for the open versions of the higher layers, and a rule for transferring lifted properties back to the standard semantics. A notion of 'control terms' reduces proof obligations to the subset of subterms that act directly (in contrast to operators for combining terms and joining processes). BibTeX: @article{AWN-AFP, author = {Timothy Bourke}, title = {Mechanization of the Algebra for Wireless Networks (AWN)}, journal = {Archive of Formal Proofs}, month = mar, year = 2014, note = {\url{https://isa-afp.org/entries/AWN.html}, Formal proof development}, ISSN = {2150-914x}, } License: BSD License Used by: AODV Status: [ok] This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.