Projektlaufzeit: 1. Februar 2018 – 31. Januar 2020.
P1-a: Modellierung der Auswirkungen konkreter Fehler in der Hardware auf die programmsichtbaren Hardwarekomponenten, sodaß daraus Fehlermodelle auf höherer Softwareebene abgeleitet werden können, die durch die Methoden der abstrakten Interpretation weiterverarbeitet werden können.
Meilensteine:
P1-b: Herstellung der Schnittstellen zwischen Astrée und den Werkzeugen von TU Kaiserslautern und Verified Systems. Spezifikation eines Austauschformates für die Übergabe korrupter Variablenwerte von FCK an Astrée, sowie die Schnittstelle zur Übergabe von Alarmen mit zugehörigen Invarianten, Kontexten und Program-Slices von Astrée an RTT-MBT. Realisierung einer automatisierten integrierten Ausführungsumgebung. Entwicklung geeigneter Visualisierungen zur Ergebnisdarstellung, darunter die Darstellung der Fehlerpropagation in Daten- und Kontrollfluß und die Rückführung von Laufzeitfehlern auf sie verursachende Hardwarefehler.
Meilensteine:
P1-c: Entwicklung eines Modells, welches die Integration der von Astrée generierten Invarianten und Warnungen in die beim BMC genutzte Transitionsrelation erlaubt. Entwicklung einer adäquaten Transitionsrelation, basierend auf einer vereinheitlichten Semantik von RTT-MBT und Astrée. Entwicklung einer Schnittstelle zur Rückführung bitpräziser Testdaten an Astrée.
Meilensteine:
P2-a: Entwicklung der Taint-Analyse für die binäre Ebene, die lokale Fehlerpropagationen mit formaler Genauigkeit nicht nur in der Hardware sondern auch in Low-Level-Softwarekomponenten bestimmt. Dies wird für eine präzise Safety-Analyse in sicherheitskritischen Treibern und für Safety-Funktionen genutzt.
Meilensteine:
P2-b: Statische Codeanalyse durch abstrakte Interpretation. Entwicklung einer für die Analyse von Hardwarefehlern spezialisierten Taint-Analyse, die den von einer Datenkorruption betroffenen Daten- und Kontrollfluß bestimmt und Alarme bei Zugriffen auf korrupte Daten aus kritischen Programmteilen erzeugt. Identifikation aller Laufzeitfehler, die aufgrund der Datenkorruption entstehen können, und Zuordnung den zugrundeliegenden Hardwarefehlern. Konzipierung eines kontextsensitiven Program-Slicers, der für einen Alarm automatisch ein bezüglich der Alarmsituation zum Eingabeprogramm äquivalentes Teilprogramm berechnet. Berechnung von Invarianten, die Informationen über Wertebereiche und Beziehungen von relevanten Programmvariablen an Alarmstellen beinhalten. Übermittlung der Alarmmeldungen mit den zugehörigen Slices und Invarianten an RTT-MBT über die in PROFORMA-1 entwickelte Schnittstelle. Erreichen einer hohen Analysepräzision, z. B. durch Modellierung der durch SEUs verursachten Werteverfälschung, oder der Einbeziehung von ggf. präziseren Invarianten des RTT-MBT-Ergebnisses in die Astrée-Analyse.
Meilensteine:
Umsetzung einer konkreten Kodierung der Programmsemantik inklusive der von Astrée ermittelten Softwareinvarianten, zur automatischen Klassifizierung der von Astrée erzeugten Warnungen. Erhöhung der Skalierbarkeit des BMC-Ansatzes, insbesondere durch Modellreduktionen und inkrementelle Lösungsverfahren.
Meilensteine: