Teilprojekt 6: Formale Verifikation unscharfer Zuverlässigkeit

Ziel dieses Teilprojekts ist die formale Modellierung, Formulierung und Verifikation von Systemeigenschaften in drahtlosen Ad-hoc-Netzen wie z.B. Reaktionszeit, Erreichbarkeit von Zielknoten und Energieverbrauch auf der Grundlage automatentheoretischer Konzepte. Die besonderen Herausforderungen liegen zum einen in der Modellierung temporaler Aspekte und zum anderen darin, dass die Ergebnisse der Analyse nicht in Ja-Nein-Antworten gegeben werden sollen, sondern in Form von Wahrscheinlichkeitsaussagen oder unscharfer Zuverlässigkeitsniveaus.

Model Checking for Energy Efficient Scheduling in Wireless Sensor Networks

Im Kontext des ZeuS Projekts (Zuverlässige Informationsbereitstellung in energiebewussten ubiquitären Systemen) wurden erste Fallstudien WS07b abgeschlossen, die den Energieverbrauch einzelner Sensorknoten untersuchen. Die Kommunikation basiert auf dem IEEE 802.15.4 Standard (ZigBee basierend) und wird als beacon-disabled modelliert. Das so entstehende vielseitig anwendbare und flexible System basiert auf Basis von Timed Automata Theorie und wurde mit Hilde des Uppaal Tools analysiert. Durch die erschöpfende Analyse des Zustandsraum der durch die Modellierung generiert wird, lassen sich insbesondere selten auftretende Eigenschaften aufzeigen.

Analyse von authentifizierter Anfrageflutung durch probabilistische Methoden

Sichere Kommunikation ist ein elementarer Bestandteil im Bereich von Drahtlosen Sensornetzen, die eine Vielzahl von Sicherheitsmechanismen und -methoden ansprechen. Da diese Sicherheit mit der knappen Ressource Energie einhergeht, ist die Anstrengung in diesem Kontext die Sicherheit zu maximieren und gleichzeitig energiebewusst zu arbeiten. Durch die Wahl formaler Methoden können probabilistische Protokolle und Methoden besonders erschöpfende und effizient untersucht werden WS07a, WS08, da man alle Einflüsse eines Protokolls untersucht und nicht nur jene, die am häufigsten auftreten (vgl. Simulation). So müssen Experimente eine genügend hohe hohe Wiederholung aufweisen, um einen gewünschten Grad an Konfidenz zu erhalten.

TP6-AQFEnergyTradeoff.jpg
Lösung des Energie/Sicherheits-Tradeoff durch probabilistische Modellprüfung

Qualitative Untersuchungen von Protokollen und Software

Im Bereich der Verifikation von Korrektheitsaussagen wurde ein Protokoll zur sicheren Anfrageflutung (sAQF) auf Grundlage automatentheoretischer Modelle untersucht WB09. Durch Verifikation konnten hierbei Fehler in einer Formel aufgedeckt werden die zur Quantifizierung des Ansatzes -- also zum Vergleich mit anderen Protokollen -- benutzt wird. Eine korrekte Formulierung des Sachverhalts basierend auf der hyper-geometrischen Verteilung wurde hergeleitet und mithilfe von Verifikationsverfahren bewiesen. Darüber hinaus wurden Fehler in einem Simulationsskript entdeckt, die vermutlich ohne die Anwendung formaler Hilfsmittel verborgen geblieben wären.

Da händisch modellierte Systeme stets mit einem erheblichen Designaufwand verbunden sind, wurde eine Abstraktionstechnik untersucht, mit deren Hilfe sich Verhaltensmodelle direkt aus Sensorknotensoftware in TinyOS generieren lässt. Der Prozess der automatischen Modellgenerierung eröffnet insbesondere den Weg für Programme -- die in TinyOS implementiert sind -- mit Hilfe formaler Verifikationstechniken zu überprüfen.

Angewendet wurde die Modellgenerierung auf ESAWN BWZ06, ein Protokoll das von TP3 entwickelt wurde. Mit Hilfe von Software Bounded Model Checking WP09 (SBMC) konnte nicht nur Software-Sicherheit, d.h. typ-korrekte Dereferenzierung von Zeigern, Null-Division u.s.w. bewiesen werden. Auch Protokoll relevante Eigenschaften wurden spezifiziert und verifiziert. Da sich hierdurch hauptsächlich sequentielle Eigenschaften des ESAWN Protokolls beweisen lassen wurde ein nebenläufiges Modell modelliert und in WS09 verifiziert. Neben der Analyse durch SBMC wurden auch Verifikationswerkzeuge wie VCC gemäß dem ``Design-By-Contract''-Ansatz angewendet. Als Ausgangspunkt für die Verifikation diente das generierte Modell des ESAWN Protokolls aus TinyOS.

TinyOSabstraction.png
Abstraktion von Protokollen aus TinyOS als Grundlage für Software Bounded Model Checking (SBMC)

Auch Software anderer Entwicklungsplattformen, waren Bestandteil der Untersuchungen. Ein Beispiel hierfür sind die Sun SPOTS, die eine virtuelle Maschine besitzen und die Ausführung eines Java Dialekts erlauben. So wurde in Scheben08 quell-offene Teile der SPOTs Bibliothek auf Korrektheit überprüft. Dies geschah durch Spezifikationen aus verfügbaren Hersteller Dokumenten und dem Quellcode und die anschließende Verifikation wurde mit Hilfe eines Theorembeweisers durchgeführt.

 
Mail to webmaster