Mechanizing a Process Algebra for Network Protocols

Timothy Bourke 1, 2 Robert Van Glabbeek 3, 4 Peter Höfner 3, 4
2 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, CNRS - Centre National de la Recherche Scientifique, Inria de Paris
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 composi-tional technique for lifting global invariants stated at the level of individual nodes to networks of nodes.
Type de document :
Article dans une revue
Journal of Automated Reasoning, Springer Verlag, 2016, 56, pp.309-341. <10.1007/s10817-015-9358-9>
Liste complète des métadonnées


https://hal.inria.fr/hal-01408217
Contributeur : Timothy Bourke <>
Soumis le : samedi 3 décembre 2016 - 16:44:39
Dernière modification le : mardi 6 décembre 2016 - 01:05:58
Document(s) archivé(s) le : jeudi 23 mars 2017 - 00:32:22

Fichier

final.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Timothy Bourke, Robert Van Glabbeek, Peter Höfner. Mechanizing a Process Algebra for Network Protocols. Journal of Automated Reasoning, Springer Verlag, 2016, 56, pp.309-341. <10.1007/s10817-015-9358-9>. <hal-01408217>

Partager

Métriques

Consultations de
la notice

103

Téléchargements du document

30