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{http://isa-afp.org/entries/AWN.html},
Formal proof development},
ISSN = {2150-914x},
}
|