Siemens-Preis

2009 |

Bulwahn, Lukas; Böck, Heiko

Preisstifter und Preisträger des Absolventenfestes 2009, Bildnachweis: Maxmilian Geuter

Lukas Bulwahn wurde für seine Diplomarbeit: Code Generation from Inductive Predicates in Isabelle/HOL der mit 1.000 Euro dotierte Siemens-Preis verliehen.

Laudatio:

Isabelle ist ein interaktiver Beweisassistent. Darin können logische Aussagen formuliert und bewiesen werden.

Ein wichtiges Einsatzgebiet von Isabelle ist die Verifikation funktionaler Programme. Daher unterstützt das System den Export von Gleichungsspezifikationen in funktionale Programmiersprachen mittels eines Code-Generators.  Gleichungsspezifikationen sind allerdings nicht die einzig angewandte Spezifikationstechnik in Isabelle - fast genauso wichtig sind induktiv definierte Prädikate. Entsprechen Gleichungsspezifikationen am ehesten Programmen in ML und Haskell, so sind induktiv definierte Prädikate am besten mit Prolog-Programmen zu vergleichen.

An dieser Stelle setzt die Diplomarbeit an. Sie beschreibt eine Übersetzung induktiv definierter Prädikate in Gleichungsspezifikationen. Jeder Übersetzungsschritt wird dabei formal im System bewiesen, das heißt es ist garantiert, dass die erstellte Gleichungsspezifikation aus der ursprünglichen, induktiv definierten folgt. Die Gleichungsspezifikationen lassen sich dann konventionell mittels eines Code-Generators in funktionale Programmiersprachen übersetzen.

Damit wird es möglich, induktive Spezifikationen als funktionale Programme auszuführen. In anderen Worten, die programmiersprachliche Ausdrucksfähigkeit von Isabelle, vorher auf ML-ähnliche Programme beschränkt, ist auf Prolog-artige Programme erweitert worden, ohne dass korrektheitskritische Komponenten modifiziert werden mussten.

Heiko Böck wurde für seine Diplomarbeit: Demonstration eines Gateways für zeit- und ereignisgesteuerte Feldbusse der mit 1.000 Euro dotierte Siemens-Preis verliehen.

Laudatio:

Herr Böck beschäftigte sich in seiner Arbeit mit der Entwicklung eines Gateways für zeit- und ereignisgesteuerte Feldbusse in der Triebwerksregelung. Während in vielen Bereichen, vor allem im Automobilbereich, bereits verteilte Regelungen auf Basis eines Bussystems zum Einsatz kommen, findet in der Triebwerksregelung bis heute die zentrale Regelung Anwendung. Sensoren und Aktuatoren sind über analoge Verbindungen direkt mit dem zentralen Steuergerät verbunden. Mit steigenden Anforderungen an zukünftige Triebwerksregler stößt man mit der zentralen Regelung an die Grenzen der Machbarkeit. Zur funktionalen Umsetzung kommen außerdem Aspekte wie die Wiederverwendbarkeit von Komponenten oder die Gewichtseinsparung hinzu.

Am Beispiel eines verteilten Regelungssystems (DCS, distributed control system) sollten im Rahmen der Arbeit zentral verwaltete Aufgaben auf mehrere autarke Regelungseinheiten bzw. intelligente Aktuatoren verteilt werden. Der erforderliche Datenaustausch sollte über Bussysteme, die je nach Anwendungszweck unterschiedlich ausgelegt werden können, erfolgen. Zur Verbindung von verschiedenen Bussystemen sollte ein intelligentes Gateway eingesetzt werden, dass sowohl zeit- als auch ereignisgesteuerte Kommunikationsprotokolle unterstützt.

Im ersten Teil der Arbeit wurden acht für die Luftfahrt relevante Bussysteme sehr ausführlich untersucht. Dabei betrieb Herr Böck eine sehr intensive und ausführliche Literaturrecherche und sammelte in Zusammenarbeit mit Anwendern die notwendigen Informationen. Resultat sind ein umfassender Vergleich und eine Bewertung der Protokolle inklusive Erörterung der individuellen Eigenschaften. Diese Evaluierung schaffte die Entscheidungsgrundlage für die Auswahl von geeigneten Bussystemen zur Umsetzung der verteilten Triebwerksregelung. Neben diesen theoretischen Grundlagen, konzipierte und implementierte Herr Böck in der Arbeit auch einen Gateway Prototyp basierend auf einem TTP Development Cluster und einem CAN-Bus. Der CAN Bus wurde dabei vornehmlich für Überwachungszwecke und der TTP/C Bus für Regelungszwecke eingesetzt.
Zunächst wurden die Anforderungen in Absprache an das Gateway mit den Anwendern definiert und auf deren Basis dann die Architektur konzipiert.

Die Implementierung des Gateways erfolgte dabei über eine statische Konfiguration, d. h. sämtliche Nachrichten, welche das Gateway passieren sollen, sind vorbestimmt. Auf diese Weise wurde das zwingend notwendige deterministische Verhalten des Gateways erreicht. Durch einen Prüfplan, der
alle notwendigen Anwendungsfälle abdeckt, konnte die korrekte Funktionsweise des Gateways verifiziert werden.

Ergebnis der Arbeit ist ein funktionsfähiges Gateway für den TTP/C und den CAN Bus. Dabei wurde das Gateway so generell und modular wie möglich umgesetzt, sodass ein Einsatz von anderen Bussystemen und auch Betriebssystemen leicht möglich sein dürfte. Die Datenstrukturen für die Konfiguration wurden so konzipiert, dass die Konfiguration auf einfache Weise durch einen Code Generator erstellt werden kann, um damit die Integrität des Gateways sicherzustellen.

Herr Böck brachte in seine Arbeit sein großes Fachwissen im Bereich der Informatik ein und erarbeitete sich neue Wissensgebiete eigenständig. Die Ergebnisse der Arbeit ermöglichen der Avionik-Industrie, aber auch anderen Industriezweigen, eine wesentliche Flexibilisierung der Regelungsaufgaben. Somit erlaubt die Arbeit die kostengünstige Umsetzung von neuartigen, innovativen Architekturen.