FWF - QUAINT - Quant. Entscheidungsprozeduren Interpolation f. Korrektur

  • Hofferek, Georg, (Teilnehmer (Co-Investigator))
  • Könighofer, Robert, (Teilnehmer (Co-Investigator))
  • Bloem, Roderick (Projektleiter (Principal Investigator))

Projekt: Foschungsprojekt

Beschreibung

Trotz aller Anstrengungen die in die Verifikation gesteckt werden, ist der Entwurf integrierter Schaltkreise so
komplex geworden, dass kritische Fehler oft ihren Weg bis ins Silizium finden. Abgesehen von Fehlern, die einen
Totalausfall bzw. die Nichteinsetzbarkeit des Systems zur Folge haben, sind Änderungen an der Hardware nach
Beginn der Produktion im Regelfall aber zu teuer. Bei Systemen, die sowohl Hardware- als auch
Softwarekomponenten enthalten, gibt es daher oft den Bedarf nach Software-Abhilfen für Fehler in der Hardware.
Im Rahmen des QUAINT Projekts schlagen wir vor automatische Methoden zur Erstellung solcher Abhilfen zu
entwickeln. Wir werden das Reparatur-Problem von zwei Seiten betrachten. Einerseits werden wir Methoden zur
Modellierung von Hardwarefehlern entwickeln, so dass die Suche nach einer Software-Abhilfe möglich wird. Die
Aufgaben umfassen die Fehlerlokalisierung und das Lösen von Formeln für eine gültige Reparatur. Aufbauend auf
frühere Arbeiten betrachten wir das Reparatur-Problem als ein Spiel von zwei Spielern (der Umgebung und des
Systems), die mit entgegengesetzten Interessen spielen (die Spezifikation zu verletzen, bzw. zu erfüllen). So wird
das Reparatur-Problem ganz natürlich zu Formeln mit Quantoren-Alternierung führen. Allerdings sind Änderungen
nötig sind, um gegebene Hardware-Einschränkungen zu berücksichtigen. Das zweite Ziel ist es, neue Methoden zu
entwickeln, um solche Formeln effizient auszuwerten und Reparaturen aus ihnen zu extrahieren. Hier werden wir
unser bestehendes Wissen über Interpolation für die Extraktion von Funktionen und Quantorenelimination zur
Beschleunigung des Lösens von QBF-Problemen verwenden, um Zertifikate, die für effiziente Reparaturen
verwendet werden können, zu generieren. Wir werden auch untersuchen, wie man sich über die Bit-Ebene hinaus
bewegen kann und werden quantifizierte Formeln in anderen Logiken, insbesondere unter Verwendung von
Äquivalenz-Logik und Logik der Uninterpretierten Funktionen studieren.
StatusAbschlussdatum
Tatsächlicher Beginn/ -es Ende1/01/1230/09/15