Mechanizing a process algebra for network protocols

DOI10.1007/S10817-015-9358-9MaRDI QIDQ287372zbMATH OpenOpenAlexFDO

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

Publication date 26 May 2016

Published in Journal of Automated Reasoning (Search for Journal in Brave)

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

zbMATH Keywords

process algebracompositional invariant proofsinteractive theorem provingIsabelle/HOLmobile ad hoc networkswireless mesh networks

Mathematics Subject Classification ID

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

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.

Recommendations

• Showing invariance compositionally for a process algebra for network protocols
• A process algebra for wireless mesh networks
• Proving properties of dynamic process networks
• Mechanizing compositional reasoning for concurrent systems: some lessons
• Compositional verification of a communication protocol for a remotely operated aircraft

Cites work

• scientific article; zbMATH DE number 5604105 (Why is no real title available?)
• scientific article; zbMATH DE number 4110131 (Why is no real title available?)
• scientific article; zbMATH DE number 1277257 (Why is no real title available?)
• scientific article; zbMATH DE number 1082078 (Why is no real title available?)
• scientific article; zbMATH DE number 194539 (Why is no real title available?)
• scientific article; zbMATH DE number 3302923 (Why is no real title available?)
• A Calculus for Mobile Ad Hoc Networks
• A framework for security analysis of mobile wireless networks
• A mechanized proof of loop freedom of the (untimed) AODV routing protocol
• A process algebra for wireless mesh networks
• A process calculus for mobile ad hoc networks
• A structural approach to operational semantics
• An observational theory for mobile ad hoc networks (full version)
• Concurrency verification. Introduction to compositional and noncompositional methods
• Extending Sledgehammer with SMT solvers
• Isabelle/HOL. A proof assistant for higher-order logic
• Isabelle/jEdit – A Prover IDE within the PIDE Framework
• Psi-calculi in Isabelle
• Shared-memory multiprocessing for interactive theorem proving
• Showing invariance compositionally for a process algebra for network protocols
• Temporal verification of reactive systems: response
• The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
• Towards a calculus for wireless systems

Cited in

(4)

• Analysing AWN-Specifications Using mCRL2 (Extended Abstract)
• Depletable channels: dynamics, behaviour, and efficiency in network design
• Showing invariance compositionally for a process algebra for network protocols
• Compositional verification of a communication protocol for a remotely operated aircraft

Describes a project that uses

Uses Software

• Coq
• Isabelle/HOL
• TPTP
• PIDE
• Isabelle/jEdit
• Sledgehammer
• Locales
• UNITY
• Isabelle/Circus
• Psi-calculi
• Archive Formal Proofs
• AODV
• AWN

This page was built for publication: Mechanizing 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 Q287372)