Inkrementelle Entwicklung, kontinuierliche Überprüfung: Software Model Checking von temporären HAL- Schnittstellenspezifikationen für eingebettete Systeme mit Hardware-Abstraktionsschicht

• Antragsteller: Professor Dr. Andreas Podelski; Professor Dr.-Ing. Axel Sikora
• Fachliche Zuordnung: Softwaretechnik und Programmiersprachen
• Förderung: Förderung seit 2022
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 503812980

Wir untersuchen das Potenzial von Software Model Checking (einem Paradigma für Black-Box-Verifikationswerkzeuge, die auf der automatischer Abstraktion nach dem CEGAR Prinzip basieren) in einem neuen Ansatz. Die Idee ist, den Softwareentwicklungsprozess an die Fähigkeiten des Software Model Checking anzupassen (im Gegensatz zu dem eher üblichen Ansatz, den Verifikationsprozess an die Softwareentwicklung anzupassen). Der konkrete Kontext, in dem wir die Forschung durchführen, ist die Entwicklung von Anwendungsprogrammen für eingebettete Systeme mit der Garantie der Abwesenheit von Verletzungen von temporalen Spezifikationen für die Schnittstelle mit der Hardware Abstraktionsschicht.

• DFG-Verfahren: Sachbeihilfen