Trustworthy Systems

Mechanizing a process algebra for network protocols

Authors

Timothy Bourke, Rob van Glabbeek and Peter Hoefner

INRIA
France

Ecole normale supérieure

NICTA

UNSW

Abstract

This paper presents the mechanization of a process algebra for Mobile Ad hoc Networks and Wireless Mesh Networks, and the development of a compositional framework for proving invariant properties. Mechanizing the core process algebra in Isabelle/HOL is relatively standard, but its layered structure necessitates special treatment. The control states of reactive processes, such as nodes in a network, are modelled by terms of the process algebra. We propose a technique based on these terms to streamline proofs of inductive invariance. This is not sufficient, however, to state and prove invariants that relate states across multiple processes (entire networks). To this end, we propose a novel compositional technique for lifting global invariants stated at the level of individual nodes to networks of nodes.

BibTeX Entry

  @article{Bourke_GH_16,
    author           = {Bourke, Timothy and van Glabbeek, Robert and H\"ofner, Peter},
    doi              = {10.1007/s10817-015-9358-9},
    journal          = {Journal of Automated Reasoning},
    keywords         = {interactive theorem proving; isabelle/hol; process algebra; awn; wireless mesh networks; mobile
                        ad-hoc networks; compositional invariant proofs},
    month            = mar,
    number           = {3},
    pages            = {309--341},
    paperurl         = {https://trustworthy.systems/publications/nicta_full_text/8466.pdf},
    title            = {Mechanizing a Process Algebra for Network Protocols},
    volume           = {56},
    year             = {2016}
  }

Download