Formales Zeitanalyseframework für Echtzeitsysteme (FORTAS-RT

Das Projekt FORTAS beschäftigt sich mit der Laufzeitanalyse von Embedded Software, speziell der Analyse von in C geschriebener Steuerungssoftware. In vielen wichtigen Industriebereichen wie etwa der Automobilindustrie ist die zeitliche Korrektheit von Steuerungssoftware ein wesentliches Qualitätsmerkmal, um die Sicherheit der Insassen eines Fahrzeuges zu gewährleisten. Das Projekt FORTAS trägt den Industrieanforderungen nach einem Software-Engineering-orientieren Zeitanalysetool Rechnung, welches die Lücke schließt zwischen dem höchst unzuverlässigen ad hoc Testen und der klassischen statischen Zeitanalyse, welche, da sie primär auf Analyse der maximalen Ausführungszeit ausgelegt ist, detailliertes Wissen über die Zielhardware und signifikanten Benutzeraufwand benötigt. Das Projekt vereint die orthogonalen Expertisen der Gruppe für Echtzeitsysteme der Technischen Universität Wien und die Gruppe für Theoretische Informatik der Technischen Universität München. Technisch gesprochen benutzt FORTAS Abstraktionsmethoden aus dem Bereich Model Checking von Software, um damit von Programmen automatisch und unabhängig von der Zielhardware Testdaten abzuleiten. Durch systematische Testläufe auf der Zielplattform werden Zeitinformationen gesammelt, und daraus ein Zeitmodell in Form einer annotierten Zustandsmaschine berechnet. Um die geforderte Granularität zu erreichen, wird dieser Prozess innerhalb einer Verfeinerungsschleife iteriert.

Das Projekt FORTAS beschäftigt sich mit der Laufzeitanalyse von Embedded Software, speziell der Analyse von in C geschriebener Steuerungssoftware. In vielen wichtigen Industriebereichen wie etwa der Automobilindustrie ist die zeitliche Korrektheit von Steuerungssoftware ein wesentliches Qualitätsmerkmal, um die Sicherheit der Insassen eines Fahrzeuges zu gewährleisten. Das Projekt FORTAS trägt den Industrieanforderungen nach einem Software-Engineering-orientieren Zeitanalysetool Rechnung, welches die Lücke schließt zwischen dem höchst unzuverlässigen ad hoc Testen und der klassischen statischen Zeitanalyse, welche, da sie primär auf Analyse der maximalen Ausführungszeit ausgelegt ist, detailliertes Wissen über die Zielhardware und signifikanten Benutzeraufwand benötigt. Das Projekt vereint die orthogonalen Expertisen der Gruppe für Echtzeitsysteme der Technischen Universität Wien und die Gruppe für Theoretische Informatik der Technischen Universität München. Technisch gesprochen benutzt FORTAS Abstraktionsmethoden aus dem Bereich Model Checking von Software, um damit von Programmen automatisch und unabhängig von der Zielhardware Testdaten abzuleiten. Durch systematische Testläufe auf der Zielplattform werden Zeitinformationen gesammelt, und daraus ein Zeitmodell in Form einer annotierten Zustandsmaschine berechnet. Um die geforderte Granularität zu erreichen, wird dieser Prozess innerhalb einer Verfeinerungsschleife iteriert.