Protocol design, development and standardisation still follow the lines of rough consensus and running code. This approach yields fast and impressive results in the sense that protocols are actually implemented and shipped, but comes at a price. Protocol specifications, which are mainly written in natural languages without presenting a formal specification, are (excessively) long, ambiguous, underspecified and erroneous. These shortcomings are neither new nor surprising, and well documented.
It is the purpose of this talk to provide further evidence that formal methods in general and process algebras in particular can overcome these problems. They provide powerful tools that help to analyse and evaluate protocols, already during the design phase. To illustrate this claim, I report how a combination of pen-and-paper analysis, model checking and interactive theorem proving has helped to perform a formal analysis of the Ad hoc On-Demand Vector (AODV) routing protocol. The talk concludes with a brief discussion on how the AODV case study has influenced my current and future research.
Peter Höfner is principal research scientist at Data61, CSIRO, Australia's leading data innovation group. He is also conjoint Associate Professor at the University of New South Wales, Australia.
His research focuses on applications of formal methods in informatics, including protocol verification, software engineering and hybrid system analysis. Main focus lies on algebraic calculi for these topics. He (co-)authored over 60 refereed papers in international journals and conferences. For his PhD thesis he received an award for young researchers of the Universität Bayern e.V. He is editor of the Journal of Logic and Algebraic Methods in Computer Science, and member of the IFIP Working Groups 2.1 (Algorithmic Languages and Calculi) and 2.3 (Programming Methodology).