Feb 07, 2017: Peter Hoefner: Using Process Algebra to Design Better Protocols

February 07, 2017Using Process Algebra to Design Better Protocols
Room: HB 2CPeter Hoefner

"Despite the maturity of formal description languages and formal methods for analyzing them, the description of real protocols is still overwhelmingly informal. The consequences of informal protocol description drag down industrial productivity and impede research progress" Pamela Zave

This talk advocates formal methods in general, and process algebra in particular, as an alternative methodology for specifying, analysing and verifying protocols.

After a short introduction of "failures" in specifying protocols, I will give a brief overview of our work in this area, which includes the development of a process algebra for wireless networks, and its application to prove loop freedom of the AODV routing protocol, one of the major protocols in the area of wireless mesh networks. The latter required some adaptations to the specification, as the original specification protocol was not loop free.

I will show that our modular proof strategy makes it easy to check that crucial correctness properties, such as loop freedom, are preserved under changes in the specification. Through automatic translation from process-algebraic specifications into the input language of model checkers, such as UPPAAL, proposed specifications can be tested on the fly model-checking techniques.