FWF - QUAINT - Quant. Entscheidungsprozeduren Interpolation f. Korrektur

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.