Technische Universität München, Institut für Informatik
DIPLOMARBEIT in Zusammenarbeit mit Validas AG :
Validierung von Verteilten Componenten: Kopplung von AutoFocus und Spin
Thematische Einordnung:
AutoFocus ist ein mehrfach ausgezeichnetes Werkzeug zur Entwicklung und
Validierung von Systemen, das von dem Startup Validas AG vermarktet und
weiter entwickelt wird. AutoFocus basiert auf einer graphischen Darstellung von
Koponenten. Spin
ist ein Model Checking Werkzeug, mit dem
sich Systeme automatisch auf bestimmte Eigenschaften prüfen lassen.
Im Gegensatz zu anderen an AutoFocus angebundenen Model Checkern
verwendet Spin ein anderes in vielen Situationen effizienteres Prüfverfahren.
Konkrete Aufgabenstellung:
Im Rahmen der Arbeit soll eine Kopplung von AutoFocus an Spin konzipiert
und realisiert werden. Ferner sollen das Ergbnis anhand von Beispielen
mit den beiden anderen Model Checker Anbindungen verglichen werden.
Die Kopplung soll in Java erfolgen.
Gute Betreuung durch die TU-Mitarbeiter und die Validas AG ist gesichert.
Voraussetzungen:
Java, Logik, Software-Engineering.
Möglichkeiten:
Erlernen neuester Methoden im SWE, Konzipieren UND Programmieren, Erfahrungen bei einer Startup-AG
Betreuer:
Validas AG: Dr. Oscar Slotosch slotosch@validas.de, Tel.: 89051894
Guido Wimmel
Alexander Pretschner
Alexander Wisspeintner
Aufgabensteller:
Prof. Dr. Manfred Broy