Showing invariance compositionally for a process algebra for network protocols

DOI10.1007/978-3-319-08970-6_10zbMATH Open1416.68153arXiv1407.3519OpenAlexW85190413MaRDI QIDQ2879249FDOQ2879249

Authors: Timothy Bourke, Peter Höfner, Rob van Glabbeek

Publication date: 8 September 2014

Published in: Interactive Theorem Proving (Search for Journal in Brave)

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.

Full work available at URL: https://arxiv.org/abs/1407.3519

Recommendations

Mathematics Subject Classification ID

Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Network protocols (68M12)

Cited In (3)

Uses Software

This page was built for publication: Showing invariance compositionally for a process algebra for network protocols

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2879249)