Entwicklung zuverlässiger eingebetteter Systeme in einer modularen Verifikationsumgebung

• Antragstellerin: Professorin Dr.-Ing. Paula Herber
• Fachliche Zuordnung: Rechnerarchitektur, eingebettete und massiv parallele Systeme
• Förderung: Förderung von 2013 bis 2021
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 234310760

Eingebettete Systeme werden häufig in sicherheitskritischen Anwendungen eingesetzt, zum Beispiel in Autos, Flugzeugen oder Verkehrssteuersystemen. Ihre Korrektheit ist deshalb äußerst wichtig um massive finanzielle Verluste oder sogar Verletzungen und Todesfälle zu vermeiden. Die Verifikation eingebetteter Systeme ist jedoch nicht trivial, insbesondere weil diese Systeme sehr komplex sind, auf beschränkten Ressourcen laufen und typischerweise aus eng miteinander verflochtenen Hardware- und Softwareanteilen bestehen. Um diesem Problem zu begegnen wollen wir eine modulare Verifikationsumgebung entwickeln, die den gesamten Entwicklungsablauf digitaler HW/SW Systeme unterstützt und dabei die Verifikation von Hardware und Software-Anteilen sowie des Gesamtsystems ermöglicht. Wir zielen dabei auf Systeme ab, die in der Systembeschreibungssprache SystemC modelliert sind. SystemC ist der de facto Standard im HW/SW Co-Design, die Unterstützung automatischer und umfassender Verifikation weist jedoch gravierende Mängel auf. Als Grundlage für unseren Ansatz entwickeln wir eine formal fundierte Zwischensprache für SystemC. Darauf aufbauend entwickeln wir einerseits modulare Abstraktionswerkzeuge, mit denen der Zustandsraum signifikant verkleinert werden kann, und andererseits Transformationswerkzeuge für verschiedene Verifikationswerkzeuge. Insbesondere kombinieren wir dabei Hardware-, Software- und System-Verifikationstechniken um mit den verschiedenen semantischen Modellen umgehen zu können, die in eingebetteten Systemen inhärent miteinander verschlungen sind. Ein weiterer wichtiger Beitrag ist eine Technik zur automatischen Auswahl und Kombination dieser Werkzeuge.

• DFG-Verfahren: Sachbeihilfen