### 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).

### License

BSD License

### Topics

- Computer science/Concurrency/Process calculi

### Session AWN

- Lib
- TransitionSystems
- Invariants
- OInvariants
- AWN
- AWN_SOS
- AWN_Cterms
- AWN_Labels
- Inv_Cterms
- AWN_SOS_Labels
- Pnet
- Closed
- OAWN_SOS
- OAWN_SOS_Labels
- OPnet
- ONode_Lifting
- OPnet_Lifting
- OClosed_Lifting
- AWN_Invariants
- OAWN_Invariants
- OAWN_Convert
- Qmsg
- Qmsg_Lifting
- OClosed_Transfer
- AWN_Main
- Toy
- AWN_Term_Graph

### Used by

- Loop freedom of the (untimed) AODV routing protocol

## Cite

×

AWN-AFP

    @article{AWN-AFP,
      author  = {Timothy Bourke},
      title   = {Mechanization of the Algebra for Wireless Networks (AWN)},
      journal = {Archive of Formal Proofs},
      month   = {March},
      year    = {2014},
      note    = {\url{https://isa-afp.org/entries/AWN.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Feb 22, 2016 : Isabelle2016
- May 27, 2015 : Isabelle2015
- Aug 28, 2014 : Isabelle2014
- Mar 15, 2014 : Isabelle2013-2