OCG Pressemeldungen 2010
OCG Förderpreis FH 2010 vergeben
Thomas Reinbacher von der FH Technikum Wien gewinnt den Wettbewerb
Am 23. November wurde im Rahmen einer Veranstaltung der Österreichischen Computer Gesellschaft (OCG) Herr Thomas Reinbacher, MSc, mit dem Förderpreis FH ausgezeichnet.
Der Titel seiner Arbeit ist Model Checking and Static Analysis of Intel MCS-51 Assembly Code und wurde im Studiengang Master in Embedded Systems (http://embsys.technikum-wien.at) am Institut Embedded Systems an der Fachhochschule Technikum Wien von FH-Prof. DI. Dr. Martin Horauer (http://embsys.technikum-wien.at/staff/horauer) betreut.
Zum Inhalt der Arbeit:
Im Rahmen der Software-Verifikation wird kontrolliert, ob die untersuchte Software einer vorgegebenen Spezifikation entspricht und ihre Aufgaben korrekt durchführt. Diese Kontrolle ist in der Regel für eingebettete Systeme (welche in modernen Fahrzeugen, Aufzügen, Flugzeugen, Roboter, etc. eingesetzt werden) aufgrund der starken Interaktion mit ihrer Umgebung ein nicht-triviales Problem. In der industriellen Praxis wird versucht die Korrektheit von Software mittels Testen zu zeigen. Damit kann aber nur ein kleiner Prozentsatz der möglichen Fehlerquellen, die im Praxiseinsatz auftauchen können, kontrolliert werden.
Formale Ansätze, wie etwa das Model Checking erlauben es automatisiert Fehler aufzudecken, auch wenn diese in der Praxis nur äußerst selten auftreten. Dies gleicht in etwa der sprichwörtlichen Suche nach der Nadel im Heuhaufen, wobei die Nadel den Fehler darstellt. In dieser Masterarbeit werden Konzepte und Ansätze zur "Suche nach der Nadel im Heuhaufen" vorgestellt, die auf Binär-Code von eingebetteten Systemen angewendet werden können. Der Heuhaufen stellt dabei die Summe aller Zustände dar, in denen sich die untersuchte Software befinden kann und wird mit Hilfe eines Mikrokontroller-Simulators erstellt. Eine auf Binär-Code basierende Verifikationstechnik wie diese erlaubt es unter anderem auch Fehler aufzudecken, die während dem Übersetzen des Programms von einer Hochsprache (wie etwa die Programmiersprache C) in den ausführbaren Code entstanden sind.
In der Arbeit wurden Model Checking und Statische Analysen für eine Mikrocontroller Familie vorgestellt und gezeigt, wie man mittels diversen Abstraktionstechniken den zu durchsuchenden Heuhaufen drastisch verkleinern kann. In einer Kooperation mit einem Industriepartner wurde die Software für eine industrielle Webmaschine gegen eine vom Kunden aufgestellte Spezifikation verifiziert und somit die Praxistauglichkeit der Methode demonstriert. Ansätze wie dieser verfolgen langfristig das Ziel, den EntwicklerInnen von Embedded Systems Software eine automatisierte und vollständige formale Verifikationsmethode zur Verfügung zu stellen und - in letzter Instanz - auch den Endanwender mit verlässlichen und fehlerfreien Geräten zu versorgen.
Diese Arbeit entstand an dem Institut für Embedded Systems der Fachhochschule Technikum Wien in einer engen Kooperation mit dem Embedded Software Laboratory der RWTH Aachen University.
Die Österreichische Computer Gesellschaft gratuliert herzlich!
