Diese Abschlussarbeit ermöglicht erste Erfahrungen mit Industrie-Kooperationen und entsprechender Kontakte zu unserem Industriepartner. Des Weiteren können wertvolle Erfahrungen mit modernen Software-Entwicklungswerkzeugen im industriellen Umfeld gemacht werden.

Die Arbeit ist für Bachelor-, Master- oder Diplomstudierende geeignet, bei Vergabe als Bachelor-Arbeit wird das Thema auf die verkürzte Zeit angepasst.

In der Signaltechnik werden zur Steuerung des Verkehrs Mikrocontroller eingesetzt. Diese unterliegen höchsten sicherheitskritischen Anforderungen, deren Einhaltung innerhalb behördlicher Zulassungsverfahren nachgewiesen wird.

Ein Industrie-Partner des Lehrstuhls produziert solche Systeme und erfüllt die organisatorischen Voraussetzungen zur eigenverantwortlichen Durchführung der vom Gesetzgeber geforderten Prüfungen. Unser Lehrstuhl entwickelt ein System, dass in Zukunft die Prüfvorgänge unterstützen wird.

In der Regel wird ausgehend von einem Verhaltensmodell des betrachteten Systems automatisch Testfälle generiert, ausgeführt und schließlich bewertet. Hierzu werden der bekannte Modelchecker UPPAAL (http://www.uppaal.com) und zur Testausführung UPPAAL Tron eingesetzt.

Die Verhaltensmodelle werden im Idealfall aus der Spezifikation des Systems abgeleitet und dienen der UPPAAL Werkzeugkette als Eingabe. Die Vereinfachung der Modellierung steht im Zentrum dieser Arbeit.

Verschiedene Ansätze zur Reduktion des Modellierungsaufwandes werden zur Zeit untersucht. In dieser Arbeit jedoch steht die Auflösung der Komplexität der entstehenden Modelle im Vordergrund. Während der Modellierung von größeren Systemen in UPPAAL mit Hilfe von Timed Automata entstehen häufig relativ große und somit schwer erfassbare Automaten. Zur Reduktion der Komplexität wird in der Software-Technik häufig das Konzept der Modularisierung genutzt. In dieser Arbeit soll ein entsprechendes Konzept für den Bereich der Timed Automata entwickelt werden.

Dieses bedeutet, dass das Konzept der Timed Automata um weitere Elemente erweitert wird. Es sollen Module eingeführt werden, die mit definierten Schnittstellen untereinander verbunden werden können. Diese Module sollen wiederverwendbar sein, hierfür soll der Mechanismus der Instanziierung integriert werden. Die Module selber enthalten einen oder mehrere Timed Automata und kapseln somit diese Funktionalität.

Schließlich soll das neue Konzept im Rahmen einer kleinen Fallstudie evaluiert werden.

Ein funktionierendes Konzept zur Integration der Modularisierung in UPPAAL.

• Informatik Bachelor/Master/Diplom

• Software-Technik
• Automatentheorie

Christoph Pallasch

• Dr. rer. nat. Ralf Mitsching