« back

Only available in German

---

Kolloquium | SAT-basierte Diagnose für formale Eigenschaften

02.05.06 | 14:00 Uhr c.t. | Raum B2860, GW 2

Stefan Staber | TU Graz, Österreich

Zusammenfassung

Im Vortrag wird ein automatischer Ansatz zur Fehlerlokalisation für Sichrheitseigenschaften, die durch LTL-Formeln gegeben sind, vorgestellt. Wie in der modellbasierten Diagnose wird ein Fehler als Widerspruch zwischen Spezifikation und tatsächlichem Verhalten betrachtet. Dann werden Komponenten gesucht, die diese Abweichung erklären.
Die Berechnung der betreffenden Komponenten geschieht durch Abbildung auf ein Boolesches Erfüllbarkeitsproblem (SAT). Die Abbildung auf SAT und die Erweiterungen der Booleschen Formel zur Berechnung verantwortlicher Komponenten werden im Vortrag erläutert. Weiterhin werden problemspezifische Entscheidungsheuristiken für den SAT-Beweiser vorgestellt, die eine effiziente Problemlösung ermöglichen.
Der Ansatz ist sehr allgemein und dadurch nicht auf Schaltkreise beschränkt. Ich werde zeigen, wie er sich zur Fehlerlokalisation in C-Programmen einsetzen lässt.