Parameter Synthesis for Reliable, Performant and Efficient Wireless Network Protocols

• Applicant: Professor Dr. Joost-Pieter Katoen
• Subject Area: Security and Dependability, Operating-, Communication- and Distributed Systems ; Theoretical Computer Science
• Term: from 2019 to 2023
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 433044889

Contemporary wireless technologies attempt to increase the level of reliability, performance and efficiency (RPE) of their services. This can be achieved by detecting faults in a very early stage of development. Therefore, it is of utmost importance that wireless protocols meet stringent specifications about functionality (``correct delivery within a few milliseconds in 99.999\% of the cases"), particularly when these technologies are employed in safety-critical scenarios, e.g., Mobile Ad-hoc Networks (MANETs) deployed in emergency response networks. Showing that a protocol adheres to such requirements cannot be guaranteed by typical protocol analysis techniques such as simulation. More rigorous, systematic approaches are needed. Formal model-based verification has an enormous potential in this regard.This project proposes a focused research effort to develop a formal framework to assist designing new wireless network protocols with provable guarantees on RPE. This is challenging in presence of characteristics such as real-time behaviour, uncertain environments, unreliable communication, energy efficiency, etc. In order to analyse the combination of different characteristics of wireless networks and their RPE, we will focus on the model of Probabilistic Timed Automata (PTA) and their extension with prices (Priced PTA). We are in particular interested in reasoning about unknown parameters in wireless systems. That is, probabilities and costs in the protocol model are not fixed, but can instead be given as expressions over some set of model parameters. Whereas formal verification evaluates RPE for a single, fixed instantiation of system parameters, analysing parametric protocol models focuses on synthesising many - all, almost all, or optimal - parameter values that establish a given reliability or performance specification. Such analysis answers queries such as what is the tolerable message loss probability such that the protocol guarantees correct delivery?, or what is the minimal expected energy consumption while still satisfying the overall protocol specification?Parameter synthesis gives provable - and not just statistical - guarantees. By synthesising parameters fulfilling requirements optimally, we will also be able to optimise RPE, e.g., minimising expected energy consumption. We aim at developing parameter synthesis algorithms for (P)PTA where parameters can be probabilities, timings, costs, or even their combination and apply these to automatically synthesise parameter values in wireless network protocols that attain the best RPE. In order to show the feasibility of our approach, we apply our framework to redesign and develop new variants of MANET and Vehicular Ad-hoc Network (VANET) routing protocols, e.g., AODV and OLSR protocols.

• DFG Programme: Research Grants