Parameter Synthesis for Reliable, Performant and Efficient Wireless Network Protocols

• Applicant: Professor Dr.-Ing. 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

• Final Report Year: 2024

Final Report Abstract

Wireless communication is ubiquitous. It is almost continuously used by laptops and smart phones, and faces a rising popularity in production engineering (machine-tomachine) and automotive applications (vehicle-to-vehicle). Wireless communication is however subject to failure under adverse conditions. To be resilient they need to be reliable, performant and efficient. Nowadays, simulation is mostly used to analyse these characteristics before communication protocols are implemented. This comes however with important drawback: high reliability requirements require many simulation runs, comparing design alternatives is expensive, and as underlying models of simulators are often unclear, simulation results can be incomprehensible. The PASIWY project has taken a distinct approach and has focused on formal modelling and verification of reliability and performance aspects of wireless networks. Here we have proposed to follow a model-based approach where the analysis consists of three phases: developing a mathematically precise (a) model of the wireless communication protocol, and (b) description of its desired reliability and performance properties, which are then subject to (c) an automated rigorous analysis. To explore various design alternatives and find optimal tuning of the various settings in wireless communication protocols, typically many different formal analyses have to be carried out — one analysis for each setting. To remedy this, PASIWY focused on the automated synthesis of reliability and performance settings in wireless networks. That is, error probabilities (to cover the reliability aspect) and costs (modelling energy usage) in the protocol model are not fixed, but are instead given as expressions (i.e., formulas) over model parameters. We in particular considered probabilistic timed automata, an automaton-based model that can incorporate real-time aspects (such as time-out mechanisms) and uncertainty aspects (such as message loss or corruption probabilities). The essential part is that uncertainties are treated as unknowns; they are treated as parameters. The PASIWY project has developed techniques to automatically generate — all, almost all, or optimal — parameter values that establish a given reliability or performance specification. Whereas an analysis of a given concrete protocol model evaluates the reliability and performance for a single, fixed instance of system parameters, parameter synthesis focuses on synthesising (infinitely) many. Our analyses method answers queries such as what is the tolerable message loss probability such that the protocol guarantees correct delivery?, or what is the minimal such loss probability while ensuring an acceptable delivery service? Concretely, we have developed formal models of two prominent wireless routing protocols with their required properties, novel algorithmic techniques for parameter synthesis of parametric timed automata, and realised them in a prototypical software tool.

Publications

• Probabilistic Model Checking of AODV. Lecture Notes in Computer Science, 54-73. Springer International Publishing.
  Kamali, Mojgan & Katoen, Joost-Pieter
  
• Tweaking the Odds in Probabilistic Timed Automata. Lecture Notes in Computer Science, 39-58. Springer International Publishing.
  Hartmanns, Arnd; Katoen, Joost-Pieter; Kohlen, Bram & Spel, Jip
  
• POMDP Controllers with Optimal Budget. Lecture Notes in Computer Science, 107-130. Springer International Publishing.
  Spel, Jip; Stein, Svenja & Katoen, Joost-Pieter
  
• Monotonicity in Markov Models. Ph.D. Dissertation, RWTH Aachen University
  Jip Spel