Im Rahmen des Austrian Computer Science Days 2015 am 15. Oktober 2015 wurde der jährlich ausgeschriebene OCG Förderpreis vergeben. Heuer teilen sich die Auszeichnung zwei Absolventen der TU Wien: Harald Beck und Robert Bill konnten im Jubiläumsjahr der TU Wien mit ihren Arbeiten punkten. [...]
Die Österreichische Computer Gesellschaft (OCG) schreibt den Förderpreis seit 1988 einmal pro Jahr für herausragende Leistungen von Studierenden an Österreichs Universitäten auf dem Gebiet der Informatik und Wirtschaftsinformatik aus. Der Förderpreis ist mit 2.000 Euro dotiert. Die OCG unterstützt damit junge Expertinnen und Experten auf diesem Gebiet.
Die Arbeit von Harald Beck trägt den Namen „Inconsistency Management for Traffic Regulations“. Worum es geht: Aus verkehrsplanerischen Zielen, der StVO, sowie Expertenwissen ergibt sich eine komplexe Logik, wie verkehrliche Einschränkungen miteinander in Beziehungen stehen können und durch Verkehrszeichen kundgemacht werden müssen. Moderne Straßenverwaltungstools, wie die Anwendung SKAT der Mödlinger Firma PRISMA Solutions, erlauben die Visualisierung solcher Daten, bilden aber ihre logischen Zusammenhänge nur teilweise ab.
In der Diplomarbeit von Harald Beck wurden deshalb Methoden entwickelt, um die Korrektheit entsprechender Datensätze automatisch überprüfen zu können, das heißt, sie bezüglich flexibler Konfliktspezifikationen evaluieren zu können. Erkannte Konflikte können auf ihre Ursachen zurückgeführt und automatisch korrigiert werden. Die resultierende prototypische Implementierung bewältigt die zentrale Herausforderung der Wartbarkeit durch die Trennung von Repräsentation und Verarbeitung des formalisierten Wissens. Theoretische Resultate spiegeln die inhärente Komplexität der Aufgabenstellungen formal wider. Die Arbeit, die am Institut für Informationssysteme der TU Wien durchgeführt wurde, illustriert darüber hinaus die Praxistauglichkeit des deklarativen Programmierparadigmas „Answer Set Programming“ zur Lösung komplexer kombinatorischer und logik-orientierter Aufgabenstellungen.
Robert Bill hat seine Arbeit „Towards Software Model Checking in the Context of Model-Driven Engineering“ genannt. Es geht darum, dass bei der Systementwicklung häufig Modelle des zu erstellenden Systems verwendet werden. Dabei können Fehler entstehen, deren Behebung teuer ist, wenn sie erst spät gefunden werden. Model Checking ist eine wichtige Verhaltensverifikationstechnik, bei der überprüft wird, ob der Anfangszustand und das Verhalten eines Systems gewisse Eigenschaften erfüllen. Die Hürde, Model Checking einzusetzen, ist aber hoch, da sich die Eingabemodelle der Model Checker häufig stark von Systemmodellen unterscheiden.
In dieser Arbeit wurde das Model-Checking-Framework MoCOCL entwickelt, das direkt mit Systemmodellen arbeitet. Es baut auf dem Eclipse Modeling Framework EMF auf und benutzt die vorhandene Modellierungssprache Ecore und die Transformationissprache Henshin zur Verhaltensspezifikation. Die Object Constraint Language OCL wurde erweitert, um Verhalten mittels CTL (Computation Tree Logic) beschreiben zu können. Diese Spezifikationen werden vom Model Checker ausgewertet, während er den Zustandsraum aufbaut. Eine Webschnittstelle ermöglicht, das Ergebnis interaktiv zu analysieren, indem Teilauswertungen der überprüften Eigenschaften, einzelne Systemzustände sowie deren Übergänge betrachtet werden können. Die Diplomarbeit wurde im Rahmen des Masterstudiums Software Engineering & Internet Computing an der TU Wien erstellt.
Übrigens: Die Ausschreibung für den OCG Förderpreis 2016 startet in Kürze. (pi/rnf)
Be the first to comment