Showing Invariance Compositionally for a Process Algebra for Network Protocols

Timothy Bourke, Robert J. van Glabbeek, Peter Höfner

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract / Description of output

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.
Original languageEnglish
Title of host publicationInteractive Theorem Proving: 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014, Proceedings
EditorsGerwin Klein, Ruben Gamboa
PublisherSpringer
Pages144-159
Number of pages16
ISBN (Electronic)978-3-319-08970-6
ISBN (Print)978-3-319-08970-6
DOIs
Publication statusPublished - 28 Jun 2014
EventThe 5th International Conference on Interactive Theorem Proving - Vienna, Austria
Duration: 14 Jul 201417 Jul 2014
Conference number: 5

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Cham
Volume8558
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

ConferenceThe 5th International Conference on Interactive Theorem Proving
Abbreviated titleITP 2014
Country/TerritoryAustria
CityVienna
Period14/07/1417/07/14

Fingerprint

Dive into the research topics of 'Showing Invariance Compositionally for a Process Algebra for Network Protocols'. Together they form a unique fingerprint.

Cite this