Seminar: Eingebettete Systeme (SS2010)

Die Programmiersprache Java ist nicht nur auf Desktoprechnern oder Servern sehr beliebt, sie ist mittlerweile auch in einigen Eingebetteten Systemen zu finden. Will man ein derartiges System verifizieren, so bietet sich Java Pathfinder als expliziter Software Model Checker für Java Bytecode an. Er ist speziell dafür konzipiert schwierig zu findende Fehler in Programmen mit mehreren Threads zu finden. Um die Verifikation von umfangreicheren Programmen zu ermöglichen, wurden im Tool eine Reihe von Heuristiken und Abstraktionsmethoden implementiert. Mit Java Pathfinder können Deadlocks und Exceptions (z.B. NullPointerException und AssertionError) erkannt werden. Außerdem kann der Nutzer selbst Eigenschaften angeben.
In diesem Vortrag sollen die Konzepte von Java Pathfinder vorgestellt werden. Außerdem soll das Tool an einer Beispielverifikation eines Java Programms vorgestellt werden. Beim Vortrag soll auch auf die Anwendbarkeit von Java Pathfinder auf Programme reeler Grösse und Beschaffenheit eingegangen werden.

Sollen mehrere verteilte Eingebettete Systeme (z.B. in Form eines drahtlosen Sensornetzwerks) kooperativ eine gemeinsame Aufgabe erledigen, so müssen die einzelnen Elemente nicht nur miteinander interagieren, sondern sich auch synchronisieren können. In der Natur lassen sich zahlreiche Beispiele für Synchronizität verteilter Komponenten finden, z.B. der Sinusknoten im Herz, das rhythmische Flackern tropischer Leuchtkäfer oder das einstimmige Zirpen von Grillen. Ein vereinfachtes mathematisches Modell der synchronisierten,  biologischen Komponenten stellen so genannte pulsgekoppelter Oszillatoren dar.
Einen anderen Aspekt verfolgt hingegen die Desynchronisation, bei der es nicht darum geht, dass alle Systemelemente synchron, zu einem bestimmten Zeitpunkt agieren, sondern im Gegenteil, dass ihre einzelnen Aktionen (zeitlich) möglichst weit voneinander stattfinden.
In diesem Vortrag sollen die formalen und begrifflichen Grundlagen für andere Seminarthemen definiert werden. Daher soll zunächst das mathematische Konzept pulsgekoppelter Oszillatoren vorgestellt sowie die Probleme bei deren Analyse erörtern werden. Außerdem soll das Konzept der Desynchronisation in diesem Zusammenhang erläutert werden.

Damit sich mehrere, verteilte Eingebettete Systeme in einem Netzwerk mittels drahtloser Kommunikation (z.B. als Sensor- oder Ad-hoc-Netzwerk) nicht zu stark interferieren, bedarf es einem gemeinsamen Protokoll zur medienzugriffs-Steuerung (engl. medium access control, kurz: MAC). Soll das MAC Protokoll robust, skalierbar und adaptiv sein, so bieten sich selbst-organisierte Ansätze an. Ein derartiger, desynchronisierter und für Multi-Hop Topologien entworfener Vertreter ist das sog. M-DESYNC Protokoll, das nach einer Explorationsphase nur mittels ortsgebundener Information den Zugriff auf das geteilte Übertragungsmedium regelt.
In diesem Vortrag soll das MAC Protokoll M-DESYNC analysiert werden. Etwaige Grundlagen, die durch vorhergehende Seminarthemen nicht abgedeckt wurden, müssen hier ebenfalls erklärt werden.

Bei den bisher betrachteten Desynchronisationsverfahren haben die Teilnehmer des Netzwerks immer nur ihre Phase angepasst. Nun kann ein Teilnehmer auber auch seine Frequenz den lokalen Gegebenheiten entsprechend verändern. Diese Desynchronisationsmethode kommt in der Natur beim Quakverhalten japanischer Baumfrösche vor und bietet neben einem selbst-organisierten Mediumszugriff auch noch die Möglichkeit, durch eingestreute Schlafzyklen Energie zu sparen.
In diesem Vortrag soll daher ein selbst-organisiertes MAC Protokoll analysiert werden, das dem Quakverhalten japanischer Baumfrösche nachempfunden ist.

Für Eingebettete Systeme existieren also zahlreiche Protokolle, die den kollisionsfreien Zugriff auf das geteilte Kommunikationsmedium kontrollieren. Einen fehlertoleranten Ansatz liefert die Desynchronisation. Aber wie "gut" ist sie? Welche Grenzen sind ihr gesetzt? Kann man durch das Einstreuen von Zufallskomponenten an geeigneten Stellen Verbesserungen erzielen?
Dieser Vortrag soll anhand mathematischer und theoretischer Überlegungen obige Fragen beantworten und zeigen, wie weit sich bei Desynchronisation Fehler minimieren lassen, wie lange es bis zum Erreichen eines konvergenten Zustands dauern kann, und welche Auswirkungen eingestreuter "Zufall" hierbei hat.

Können verteilte Eingebettete Systeme miteinander kommunizieren, dann ist aber noch lange nicht sichergestellt, dass Daten, die für einen bestimmten Netzteilnehmer gedacht sind, diesen auch erreichen. Für genau dieses Problem gibt es Routingverfahren, die auf verschiedene Weise versuchen, Daten von A nach B zu schaffen. Je nach Untersuchungsgegenstand (Energieverbrauch, Packetlatenz, max. Hop-Count, etc.) gibt es verschiedene Ansätze, die die an diese Protokolle gerichteten Erwartungen mehr oder weniger gut erfüllen. 
Da bereits bei einigen MAC Protokollen lokale Informationen über die Ein-Hop- bzw. sogar Zwei-Hop-Nachbarschaft gesammelt werden, sollen in diesem Vortrag Routingprotokolle vorgestellt werden, die von diesen bereits vorhandenen Informationen massiv Gebrauch machen. Der Vortragende soll sich daher zunächst einen Einblick in die Funktionsweise verschiedener Routingmechanismen verschaffen und anschließend einen Einblick in bestehende Routingverfahren mit lokaler Nachbarschaftsinformation erarbeiten.

Neben den auf Desynchronisation basierenden MAC Protokollen gibt es natürlich noch eine Vielzahl weiterer Protokolle. Je nach Anwendungsszenario oder Systemanforderungen sind die verschiedenen MAC Protokolle unterschiedlich gut geeignet... 
In diesem Vortrag sollen daher nochmal zwei weitere MAC Protokolle vorgestellt und analysiert werden: L-MAC und CrankShaft. Von besonderem Interesse sind hier deren unterschiedlichen Stärken und Fähigkeiten. So soll der Vortrag auch eine Gegenüberstellung beider Protokolle enthalten.

Gerade bei komplexen, eingebetteten Systemen kann man aufgrund der zahlreichen Nebenläufigkeiten manchmal nicht mehr aus dem Verhalten der einzelnen Systemkomponenten auf das Verhalten des Gesamtsystems schließen. Dieses sog. emergente Verhalten ("Das Ganze ist mehr als die Summe seiner Teile") kann man in der Natur an zahlreichen Stellen beobachten. Um sich aber als Vorgehensmodell im Bereich eingebetteter Systeme (und Sensornetze im Speziellen) zu etablieren, bedarf es formal definierter Vorgehensweisen und Entwicklungstechniken. 
Dieser Vortrag soll daher zunächst durch eine Begriffsdefinition die Abgrenzung zur Selbstorganisation schaffen und dann bereits existierende Verfahren zum Modellieren emergenten Verhaltens in Sensornetzen vorstellen.