Konstruktion und Verifikation eingebetteter echtzeitfähiger Steuerungssoftware und ihrer Transformation in ausführbaren Code unter besonderer Berücksichtigung von Multicore und Adaptivität

点击翻译按钮获取中文摘要

Ziel des Projekts ist die Entwicklung und Kombination von Grundlagen und Methoden zur Konstruktion und Verifikation eingebetteter reaktiver nebenläufiger echtzeitfähiger Software-Systeme. Derartige Systeme sollen für die gesamte Kette von Spezifikation und Quellcode bis zum von Compilern generierten, ablauffähigen Maschinencode verifiziert werden. Die Korrektheit von Software in eingebetteten sicherheitskritischen Echtzeitsystemen ist notwendige Voraussetzung für die korrekte Funktionsweise dieser Systeme, insbesondere dann, wenn ein Fehler oder Ausfall enorme negative Konsequenzen hat oder gar den Verlust von Menschenleben fordert. Satelliten, eingebettete Systeme im medizinischen Bereich oder Lotteriecomputer sind Beispiele für solche Systeme. In derartigen Systemen sind unentdeckte Fehler besonders kritisch, weil man nicht weiß, wann sie auftreten und welche Schäden sie nach sich ziehen können. Testen als Validierungsmethode kann Fehler nicht vollständig auffinden. Will man die Korrektheit der Systeme sicherstellen, muss man formal die Korrektheit der eingesetzten Software bzgl. einer zu definierenden Spezifikation zeigen. Ausgehend von der Hypothese, dass reaktive Software-Systeme in eingebetteten Systemen bestimmte Strukturen (gekennzeichnet unter anderem durch ihre Prozesse und deren Kommunikationsmuster) aufweisen, die ihre Funktionsweise charakterisieren und bei der Übersetzung in ablauffähigen Maschinencode erhalten bleiben müssen, sollen diese Strukturen am Beispiel des Betriebssystems BOSS untersucht und Methoden zu ihrer Verifikation entwickelt werden. BOSS ist ein kleines Betriebssystem für eingebettete Systeme, das von Dr. Sergio Montenegro am Fraunhofer Institut FIRST, Berlin, entwickelt wurde und bereits seit mehreren Jahren erfolgreich in verschiedenen eingebetteten Systemen verwendet wird. Da BOSS bereits bei seiner Konzeption auf eine spätere Verifikation hin angelegt wurde, eignet es sich hervorragend als Grundlage für die experimentellen Untersuchungen in dem geplanten Projekt.