Showing Invariance Compositionally for a Process Algebra for Network Protocols

Timothy Bourke 1, 2 Robert J. Van Glabbeek 3, 4 Peter Höfner 3, 4
1 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 : 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.
Type de document :
Communication dans un congrès
ITP 2014: Interactive Theorem Proving, Jul 2014, Vienna, Austria. Springer, Proceedings of the 5th International Conference on Interactive Theorem Proving (ITP 2014), 8558, pp.16, 2014, Lecture Notes in Computer Science. <http://www.cs.uwyo.edu/~ruben/itp-2014/>. <10.1007/978-3-319-08970-6_10>
Liste complète des métadonnées

https://hal.inria.fr/hal-01092348
Contributeur : Timothy Bourke <>
Soumis le : lundi 8 décembre 2014 - 15:44:50
Dernière modification le : jeudi 29 septembre 2016 - 01:22:04

Identifiants

Collections

Citation

Timothy Bourke, Robert J. Van Glabbeek, Peter Höfner. Showing Invariance Compositionally for a Process Algebra for Network Protocols. ITP 2014: Interactive Theorem Proving, Jul 2014, Vienna, Austria. Springer, Proceedings of the 5th International Conference on Interactive Theorem Proving (ITP 2014), 8558, pp.16, 2014, Lecture Notes in Computer Science. <http://www.cs.uwyo.edu/~ruben/itp-2014/>. <10.1007/978-3-319-08970-6_10>. <hal-01092348>

Partager

Métriques

Consultations de la notice

94