Förderpreisgewinner Thomas Reinbacher, MSc
Die OCG verleiht zur Förderung von hervorragenden Leistungen auf dem Gebiet der Informatik und Wirtschaftsinformatik an Studierende von Fachhochschulen jährlich den „OCG Förderpreis
FH“ für hervorragende FH-Diplom-, FH-Magister- bzw. FH-Master-Arbeiten. Der „OCG Förderpreis FH“ ist mit EUR 2.000,- dotiert und ging heuer an Thomas Reinbacher, MSc (Studiengang: Master in Embedded Systems, http:// embsys.technikumwien.at).
Model Checking and Static Analysis of Intel MCS-51 Assembly Code
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 Mikrocontroller-Simulators erstellt. Eine auf Binär-Code basierende Verifikationstechnik wie diese erlaubt es, unter anderem auch Fehler aufzudecken, die während des Übersetzens 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 diverser Abstraktionstechniken den zu durchsuchenden „Heuhaufen“ drastisch verkleinern kann. In einer Kooperation mit einem Industriepartner wurde die Software für eine industrielle Web- Maschine 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 am Institut für Embedded Systems der Fachhochschule Technikum Wien in einer engen Kooperation mit dem Embedded Software Laboratory der RWTH Aachen University.
Autor: Elisabeth Maier-Gabriel
Kontakt:
Elisabeth Maier-Gabriel
Tel.: +43 1 512 02 35-18
gabriel@ocg.at