Parametersynthese für zuverlässige, performante und effiziente Protokolle für Drahtlosnetzwerke

• Antragsteller: Professor Dr.-Ing. Joost-Pieter Katoen
• Fachliche Zuordnung: Sicherheit und Verlässlichkeit, Betriebs-, Kommunikations- und verteilte Systeme ; Theoretische Informatik
• Förderung: Förderung von 2019 bis 2023
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 433044889

• Erstellungsjahr: 2024

Zusammenfassung der Projektergebnisse

Die drahtlose Kommunikation ist allgegenwärtig. Sie wird fast ununterbrochen von Laptops und Smartphones genutzt und erfreut sich zunehmender Beliebtheit in der Produktionstechnik (Maschine-zu-Maschine) und bei Anwendungen im Automobilbereich (Fahrzeug-zu-Fahrzeug). Die drahtlose Kommunikation ist jedoch anfällig für Ausfälle unter ungünstigen Bedingungen. Um widerstandsfähig zu sein, müssen sie zuverlässig, leistungsfähig und effizient sein. Heutzutage wird die Simulation meist dazu verwendet, diese Eigenschaften zu analysieren, bevor Kommunikationsprotokolle implementiert werden. Dies bringt jedoch erhebliche Nachteile mit sich: Hohe Zuverlässigkeitsanforderungen erfordern viele Simulationsläufe, der Vergleich von Entwurfsalternativen ist teuer, und da die den Simulatoren zugrunde liegenden Modelle oft unklar sind, können die Simulationsergebnisse unerklärbar sein. Das Projekt PASIWY hat einen anderen Ansatz gewählt und sich auf die formale Modellierung und Verifizierung von Zuverlässigkeits- und Leistungsaspekten drahtloser Netzwerke konzentriert. Hier haben wir einen modellbasierten Ansatz vorgeschlagen, bei dem die Analyse aus drei Phasen besteht: Entwicklung eines mathematisch präzisen (a) Modells des drahtlosen Kommunikationsprotokolls und (b) Beschreibung seiner gewünschten Zuverlässigkeits- und Leistungseigenschaften, die dann (c) einer automatisierten rigorosen Analyse unterzogen werden. Um verschiedene Entwurfsalternativen zu untersuchen und eine optimale Abstimmung der verschiedenen Einstellungen in drahtlosen Kommunikationsprotokollen zu finden, müssen typischerweise viele verschiedene formale Analysen durchgeführt werden — eine Analyse für jede Einstellung. Um hier Abhilfe zu schaffen, konzentrierte sich PASIWY auf die automatische Synthese von Zuverlässigkeits- und Leistungseinstellungen in drahtlosen Netzen. Das bedeutet, dass die Fehlerwahrscheinlichkeiten (zur Abdeckung des Zuverlässigkeitsaspekts) und die Kosten (zur Modellierung des Energieverbrauchs) im Protokollmodell nicht feststehen, sondern als Ausdrücke (d. h. Formeln) über die Modellparameter gegeben sind. Wir haben insbesondere probabilistische Zeitautomaten betrachtet, ein auf Automaten basierendes Modell, das Echtzeitaspekte (wie Time-out-Mechanismen) und Ungewissheitsaspekte (wie Wahrscheinlichkeiten für den Verlust oder die Verfälschung von Nachrichten) einbeziehen kann. Das Wesentliche dabei ist, dass Ungewissheiten als Unbekannte behandelt werden; sie werden als Parameter behandelt. Das PASIWY-Projekt hat Techniken entwickelt, um automatisch — alle, fast alle oder optimale — Parameterwerte zu erzeugen, die eine bestimmte Zuverlässigkeits- oder Leistungsspezifikation festlegen. Während eine Analyse eines konkreten Protokollmodells die Zuverlässigkeit und Leistung für eine einzige, feste Instanz von Systemparametern bewertet, konzentriert sich die Parametersynthese auf die Synthese von (unendlich) vielen. Unsere Analysemethode beantwortet Fragen wie: Wie hoch ist die tolerierbare Verlustwahrscheinlichkeit von Nachrichten, so dass das Protokoll eine korrekte Zustellung garantiert? oder wie hoch ist die minimale Verlustwahrscheinlichkeit bei gleichzeitiger Gewährleistung eines akzeptablen Zustelldienstes? Konkret haben wir formale Modelle zweier prominenter drahtloser Routing-Protokolle mit ihren erforderlichen Eigenschaften sowie neuartige algorithmische Techniken zur Parameetersynthese parametrischer Zeitautomaten entwickelt und in einem prototypischen Software-Tool realisiert.

Projektbezogene Publikationen (Auswahl)

• 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