Projektstart: 1. Mai 2011.
Projektende: 29. April 2013.
F1.1 – „AI-basierter Nachweis funktionaler Programmeigenschaften und komponentenorientierte Analyse“ (AbsInt GmbH).
Meilenstein Q6: Konzept für AI-basierte komponentenorientierte und funktionale Verifikation (Bericht). Evaluierung anhand industrieller Fallstudie.
F1.2 – „Verifikations-/Entwurfsmodelle für Schaltungsmodule“ (TU Kaiserslautern).
Meilenstein Q4: Abstraktes Verifikations- und Automatenmodell für Schaltungsmodule auf Basis von Path-Predicate-Abstraction.
F2.1 – „Reduktion von Fehlalarmen“ (AbsInt GmbH).
Meilenstein Q4: Machbarkeitsnachweis der automatisierten Diagnosefunktionalität (Bericht).
Meilenstein Q8: Evaluierung des automatischen Annotationsassistenten anhand der fertiggestellten industriellen Fallstudie (Bericht).
F2.2 – „Komposition, Verfeinerung und Verifikation von Systemmodellen“ (TU Kaiserslautern).
Meilenstein Q8: Konzept und Implementierung eines Verfahrens zur kompositionalen Path-Predicate-Abstraction und zur Verfeinerung und Verifikation der Modelle (Bericht).
F3.1 – „Integration in den Software-Lebenszyklus“ (AbsInt GmbH).
Meilenstein Q2: Identifikation einer industrierelevanten Fallstudie als Grundlage zur Evaluierung der Projektergebnisse. Erprobung des Konzepts zur modellbasierten Codeerzeugung anhand dieser Fallstudie (Bericht).
Meilenstein Q8: Evaluierung des versionsbasierten Analysekonzepts anhand der zu F3-ABS-1 fertiggestellten Fallstudie (Bericht).
F3.2 – „Evaluierung der modellbasierten Hardwareverifikation im Gesamtfluß“ (TU Kaiserslautern).
Meilenstein Q8: Ergebnisse der modellbasierten Verifikation und Aufwände der zugehörigen Entwurfsschritte für ein industrielles Bussystem (Bericht).
F0 – Projektkoordination (AbsInt GmbH).