Projektstart: 1.9.2014.
Projektende: 1.9.2016.
F1 – Modellierung (AbsInt)
F1-a: Nebenläufige, zyklengenaue Systemmodelle als Soft-Emulator (OSS)
- F1a-T1 – Untersuchung der Modellierungsmöglichkeiten für Nebenläufigkeit
- F1a-T2 – Untersuchung der Modellierungsmöglichkeiten in SystemC
- F1a-T3 – Erstellung von handgeschriebenen C-Modellen
- F1a-T4 – Entwicklung und Evaluierung von Methoden zur automatischen Generierung von nebenläufigem SystemC
Meilensteine:
- F1a-MS1 – Spezifikation von effizienten und zyklengenauen SystemC-Modellen, Bericht: Q4
- F1a-MS1a – Zulieferung von handgeschriebenen C-Modellen als Fallbeispiel an AbsInt: Q4
- F1a-MS2 – Soft-Emulator und seine Evaluierung anhand industrieller Demonstratoren, Bericht: Q8
F1-b: Modellerzeugung für hardwarenahe Software (TUK)
- F1b-T1 – Konzept domänenübergreifender sicherer Abstraktionen für zeitabstrakte, kompositionale Hardware und Softwarekomponenten
- F1b-T2 – Entwicklung von Methodik und Technik zur Modellierung der Instruktionszellen
- F1b-T3 – Erforschung und Entwicklung eines hardware-integrierbaren Firmwaremodells
- F1b-T4 – Entwicklung von Methoden zur automatischen Optimierung der Modelle für den OSS Soft-Emulator
Meilensteine:
- F1b-MS1 – Konzept für zeitabstrakte und zyklengenaue Modellgenerierung sowie Integration in RTL-Entwürfe, Bericht: Q4
- F1b-MS2 – Modellgenerator und experimentelle Evaluierung der für den OSS-Soft-Emulator relevanten Performanzeigenschaften am Beispiel der industriellen Demonstratoren, Bericht: Q8
F1-c: Laufzeitfehleranalyse nebenläufiger Software (AbsInt)
- F1c-T1 – Entwicklung der Basistechnologie zur Nebenläufigkeitsanalyse
- F1c-T2 – Entwicklung der OSEK-Basisunterstützung und experimentelle Evaluierung anhand industrieller Fallstudie
- F1c-T3 – Vervollständigung der OSEK-Unterstützung, Entwicklung der AUTOSAR-Unterstützung und Entwicklung konzeptioneller Erweiterungen des Betriebssystemspezifikationsmechanismus
- F1c-T4 – Entwicklung von Methoden zur Steigerung der Analysepräzision auf Basis von industriellen Fallstudien und den C-Applikationen der Projektpartner TUK und OSS
Meilensteine:
- F1c-MS1 – Machbarkeitsnachweis der automatischen Laufzeitfehleranalyse für nebenläufige Software auf industrieller Fallstudie, Bericht: Q4
- F1c-MS2 – Experimentelle Evaluierung der nebenläufigen Analyse auf industriellem OSEK oder AUTOSAR Softwareprojekt sowie den Applikationen der Projektpartner, Bericht: Q8
F2: Korrektheit und Optimierung (OSS)
F2-a: Nachweis der Korrektheit der in F1-a erzeugten Modelle (OSS)
- F2a-T1 – Durchführung des Äquivalenzvergleichs von SystemC und VHDL/Verilog-Modellen
Meilensteine:
- F2a-MS1 – Vergleichsabschluß, Bericht: Q6
F2-b: Modellkorrektheit bei reaktivem Verhalten der Software mit Hardwareperipherie (TUK)
- F2b-T1 – Nutzung von Astrée bei der Erkennung nicht-funktionaler Fehler in Firmware und darauf aufbauende Konzeption und Entwicklung von Datenstrukturen für die Modellierung von Speicher, Peripherie und Zugriffssequenzen
- F2b-T2 – Integration der Datenstrukturen zur Interfacemodellierung in die Programmnetzliste
- F2b-T3 – Analyse der Adressräume und Kompaktierung des Modells für den Äquivalenzvergleich
Meilensteine:
- F2b-MS1 – Konzept für die Generierung eines funktionalen Modells für die Schnittstelle zwischen Software und Hardwareperipherie, Bericht: Q6
- F2b-MS2 – Werkzeug und Evaluierung für die Co-Verifikation von Hardware und Software mit Äquivalenzvergleich, Bericht: Q8
F2-c: Nebenläufige Fehlerklassen und Parallelisierung der Programmanalyse (AbsInt)
- F2c-T1 – Entwicklung des Konzepts für nebenläufige Fehlerklassen
- F2c-T2 – Entwicklung des Basiskonzepts zur automatischen Parallelisierung der Datenflussanalyse
- F2c-T3 – Optimierung der automatischen Parallelisierung und Realisierung weiterer Performanceverbesserungen unter Berücksichtigung industrieller Fallstudien und
der C-Applikationen der Projektpartner TUKL und OSS.
- F2c-T4 – Entwicklung von Verfahren zur Ergebnisexploration, darunter Program Slicing und dedizierte Visualisierungsverfahren; Evaluierung anhand industrieller Fallstudien.
Meilensteine:
- F2c-MS1 – Konzept für nebenläufige Fehlerklassen und parallele statische Datenflussanalyse, Bericht: Q4
- F2c-MS2 – Experimentelle Evaluierung der Erkennung von Nebenläufigkeitsfehlern und der automatischen Parallelisierung anhand industrieller Fallstudien, Bericht: Q8
F0 – Projektkoordination (AbsInt)