OCG Förderpreis FH 2010 vergeben

Thomas Reinbacher von der FH Technikum Wien gewinnt den Wettbewerb

Copyright: Österreichische Computer Gesellschaft

Wien (pts015/29.11.2010/12:47) Am 23. November wurde im Rahmen einer Veranstaltung der Österreichischen Computer Gesellschaft (OCG) Herr Thomas Reinbacher, MSc mit dem Förderpreis FH 2010 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 betreut.

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!

Über die Österreichische Computer Gesellschaft (OCG)
Als Non-Profit Organisation wirkt die Österreichische Computer Gesellschaft (http://www.ocg.at) verbindend zu einzelnen Schnittstellen des IT-Bereiches. Durch ihr ExpertInnen-Netzwerk gilt die OCG als "Brückenbauer" zwischen Professionals, Unternehmern und Wissenschaft. Nationale und internationale Konferenzen und Veranstaltungen stehen dabei im Mittelpunkt des Interesses. Mit zahlreichen Wettbewerben und Preisen fördert die OCG junger Talente. In den letzten Jahren wurde besonders der Zertifizierungsbereich erweitert. Neben dem bekannten Europäischen Computer Führerschein (ECDL) entwickelte die OCG eine Reihe eigener Zertifikate. Sie ist die österreichische Zertifizierungsstelle für alle ECDL und OCG Zertifikate. Das Ziel der OCG ist es, die Informatik als Wissenschaft umfassend und fächerübergreifend zu fördern. Besonderes Augenmerk wird aber auch auf die AnwenderInnen von Informationstechnologie gelegt. Einerseits wird die Weiterentwicklung von Technologien unterstützt und andererseits soll der Kreis der AnwenderInnen durch gezielte Maßnahmen vergrößert werden. Dabei werden auch die Auswirkungen von IT auf Menschen und Gesellschaft berücksichtigt.

Aussender:	Österreichische Computer Gesellschaft (OCG)
Ansprechpartner:	Mag. Christine Haas
Tel.:	01/512 02 35/51
E-Mail:	haas@ocg.at