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

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

Gegenwärtige Technologien für Drahtlosnetzwerke sind darauf ausgerichtet, die Zuverlässigkeit, Performanz und Effizienz (ZPE) der angebotenen Dienste zu erhöhen. Diese Ziele können durch die Erkennung von Fehlern in frühen Phasen des Systementwurfs unterstützt werden. Es ist daher wichtig, dass Protokolle für Drahtlosnetzwerke funktionale Korrektheitseigenschaften aufweisen, die durch stringente Spezifikationen ("korrekte Übermittlung innerhalb von einigen ms in 99,999% der Fälle") formalisiert sind. Dies gilt insbesondere, wenn diese Technologien in sicherheitskritischen Anwendungen eingesetzt werden, wie etwa in Mobilen Ad-hoc-Netzwerken (MANET), die als Notfall-Kommunikationsnetze verwendet werden. In solchen Fällen reichen Simulationstechniken nicht aus, um die Erfüllung der Korrektheitsanforderungen zu garantieren. Stattdessen sind präzise, systematische Ansätze erforderlich. In dieser Hinsicht hat die formale modellbasierte Verifikation ein enormes Potential aufzuweisen.In diesem Projekt schlagen wir die Entwicklung eines formalen Frameworks vor, das den Entwurfsprozess für Protokolle für Drahtlosnetzwerke mit nachweisbaren ZPE-Garantien unterstützt. Dieses Ziel stellt unter Randbedingungen wie Echtzeitverhalten, unsichere Umgebungen, unzuverlässige Kommunikation, Energieeffizienz etc. eine große Herausforderung dar. Um die Kombination verschiedener Charakteristika drahtloser Netzwerke und ihrer ZPE zu studieren, werden wir Probabilistischen Zeitautomaten (PZA) und ihrer Erweiterung um Kosten verwenden.Wir fokussieren uns insbesondere auf die Analyse unbekannter Parameterwerte in drahtlosen Systemen. Dies bedeutet, dass Wahrscheinlichkeiten und Kosten im Protokollmodell durch Ausdrücke über einer Menge von Protokollparametern gegeben sind. Während formale Verifikation die ZPE-Eigenschaften für eine einzelne, festgelegte Instanziierung von Parametern evaluiert, hat die Parameter Synthese zum Ziel, alle (oder optimale) Parameterwerte zu synthetisieren, die eine gegebene Zuverlässigkeits- oder Performanzspezifikation sicherstellen. Eine solche Analyse liefert z.B. Antworten auf die Frage nach der tolerierbaren Verlustwahrscheinlichkeit von Nachrichten, die noch eine korrekte Datenübermittlung garantiert, oder nach der die Minimierung des erwarteten Energieverbrauchs ohne Verletzung der Protokollspezifikation.Parametersynthese gibt beweisbare - und nicht nur statistische - Garantien. Unser Ziel ist die Entwicklung von Algorithmen zur Parametersynthese für PZA (mit Kosten), wobei die Parameter Wahrscheinlichkeiten, Zeitangaben, Kosten oder ihre Kombination repräsentieren, und die Anwendung dieser Verfahren zur Synthese von Parameterwerten für Protokolle für Drahtlosnetzwerke, welche die besten ZPE-Eigenschaften erzielen. Um die Durchführbarkeit unseres Ansatzes nachzuweisen, werden wir unser Framework zur Entwicklung von Varianten der MANET- und VANET (Vehicular Ad-hoc-Netzwerk)-Routingprotokolle wie AODV und OLSR einsetzen.

• DFG-Verfahren: Sachbeihilfen