Erreichbarkeitsanalyse unter Verwendung von Wortebenen-Beweisern

Im Rahmen des Projektes soll untersucht werden, wie Wortebenen-Beweiser in Verfahren zur Erreichbarkeitsanalyse eingesetzt werden können.
Das Projekt wird in Kooperation mit der Arbeitsgruppe von Prof. Andreas Veneris an der Universität Toronto durchgeführt.

Kontakt: Dr. Görschwin Fey

Der Einsatz von Schaltungen und Systemen in sicherheitskritischen Bereichen wie dem Transportwesen oder der Medizintechnik erfordert den Nachweis der Korrektheit. Aufgrund der steigenden Komplexität der Systeme kann in Zukunft nur durch den Einsatz formaler Methoden ein belastbarer Nachweis geführt werden.
Eine Basistechnik der formalen Verifikation ist die sogenannte Erreichbarkeitsanalyse. Für ein gegebenes System wird überprüft, welche Zustände erreichbar sind. So lässt sich beispielsweise beweisen, dass ein sicherheitskritischer Zustand nicht erreichbar ist. Eine weitere Anwendung ist zum Beispiel der Ausschluss falscher Gegenbeispiele (so genannter „false negatives“), die nur unter Annahme nicht erreichbarer Systemzustände auftreten. Heutige Schaltkreise werden in Hardware-Beschreibungssprachen wie VHDL, Verilog oder SystemC auf Wortebene beschrieben. Jedoch werden bisher für die Erreichbarkeitsanalyse vorwiegend Boolesche Beweisertechniken eingesetzt. Dazu gehören binäre Entscheidungsdiagramme und Boolesche Erfüllbarkeits-Beweiser. Dabei geht Wissen der Wortebene mit der Übersetzung auf Bitebene verloren. Die Ausnutzung der Wortebenen-Information wurde bereits in ersten wissenschaftlichen Veröffentlichungen untersucht – bisher stellt die Kombination von Wort- und Bitebene aber noch eine große Hürde dar.
Eine neue Art der Beweiser, so genannte Wortebenen-Beweiser, nutzen Informationen der Wortebene zusätzlich zu den etablierten Booleschen Techniken in einem einheitlichen Beweisalgorithmus. Erste Evaluationen auf allgemeinen Problemen zeigen die Effizienz dieser neuen Ansätze für allgemeingültige Probleminstanzen. Die konkrete Anwendung von Wortebenen-Beweisern auf die Erreichbarkeitsanalyse ist bisher allerdings noch unzureichend verstanden. Im Rahmen des Projektes soll untersucht werden, wie Wortebenen-Beweiser in Verfahren zur Erreichbarkeitsanalyse eingesetzt werden können.
Das Projekt wird in Kooperation mit der Arbeitsgruppe von Prof. Andreas Veneris an der Universität Toronto durchgeführt.