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.

Das Schreiben von richtiger Software oder Hardware ist sehr schwierig und Fehler können schwerwiegende Konsequenzen haben. Zum Beispiel, am 9. Mai 2015 verursachte ein Software-Problem einen Absturz eines Militär-Airbus A400M, vier Besatzungsmitglieder wurden getötet und zwei verletzt. Um solche Katastrophen zu verhindern, wollen wir Software und Hardware richtig erproben & prüfen. Der klassische Ansatz ist es, zuerst die Software zu schreiben und dann zu prüfen, aber dies scheint zu aufwendig. Es ist vorzuziehen die korrekte Software automatisch aus einer bestimmten Spezifikation zu synthetisieren. Das Synthese Problem ist ein sehr schwieriges Thema, aber in QUAINT haben wir erhebliche Fortschritte in Richtung der Umsetzung gemacht. Wir haben uns auf zwei Aspekte fokussiert: einer davon ist das Zusammenspiel zwischen Mensch und Synthese-Tools. Wir haben Synthesewerkzeuge eingebaut, die automatisch diesen Teil des Programms konstruieren, welcher für einen Programmierer besonders schwierig ist, aber nicht die Teile, die einfach sind. Wir haben auch sehr effiziente Synthese-Tools durch die Erforschung der Verbindung zwischen Synthese und unterschiedliche Logiken und Logik-Solver erstellt. Unsere taiwanesischen Partner, Experten in der Logik, waren entscheidend bei diesen Bemühungen. Schließlich hat das Projekt zur Ausbildung von zwei brillanten jungen Doktoranden beigetragen, die nun in der österreichischen Industrie arbeiten.