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 language | English |
---|---|
Title of host publication | Interactive 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 |
Editors | Gerwin Klein, Ruben Gamboa |
Publisher | Springer |
Pages | 144-159 |
Number of pages | 16 |
ISBN (Electronic) | 978-3-319-08970-6 |
ISBN (Print) | 978-3-319-08970-6 |
DOIs | |
Publication status | Published - 28 Jun 2014 |
Event | The 5th International Conference on Interactive Theorem Proving - Vienna, Austria Duration: 14 Jul 2014 → 17 Jul 2014 Conference number: 5 |
Publication series
Name | Lecture Notes in Computer Science |
---|---|
Publisher | Springer Cham |
Volume | 8558 |
ISSN (Print) | 0302-9743 |
ISSN (Electronic) | 1611-3349 |
Conference
Conference | The 5th International Conference on Interactive Theorem Proving |
---|---|
Abbreviated title | ITP 2014 |
Country/Territory | Austria |
City | Vienna |
Period | 14/07/14 → 17/07/14 |