Mechanization of the Algebra for Wireless Networks (AWN)

Timothy Bourke 1, 2, 3
3 Parkas - Parallélisme de Kahn Synchrone
DI-ENS - Département d'informatique de l'École normale supérieure, ENS Paris - École normale supérieure - Paris, Inria Paris-Rocquencourt, CNRS - Centre National de la Recherche Scientifique : UMR 8548
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).
Type de document :
Autre publication
Entry in the Archive of Formal Proofs (ISSN: 2150-914x). 2014, pp.186
Liste complète des métadonnées


https://hal.inria.fr/hal-01104031
Contributeur : Timothy Bourke <>
Soumis le : jeudi 15 janvier 2015 - 20:32:20
Dernière modification le : mercredi 28 septembre 2016 - 16:11:25
Document(s) archivé(s) le : vendredi 11 septembre 2015 - 06:53:17

Fichier

document.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01104031, version 1

Collections

Citation

Timothy Bourke. Mechanization of the Algebra for Wireless Networks (AWN). Entry in the Archive of Formal Proofs (ISSN: 2150-914x). 2014, pp.186. <hal-01104031>

Partager

Métriques

Consultations de
la notice

116

Téléchargements du document

67