Eigenschaftsbasierte Abstraktion für die formale Verifikation von Komponentensystemen

Die Qualitätssicherung ist ein wesentlicher Bestandteil bei der Entwicklung digitaler Systeme. Eine Hauptaufgabe nimmt dabei der Nachweis der funktionalen Korrektheit ein. Dazu wird üblicherweise die Simulation eingesetzt, mit der auf Fehler im Entwurf des Systems getestet, die Fehlerfreiheit jedoch nicht garantiert werden kann. Für die Verifikation von sequentiellen Schaltungen werden daher immer häufiger formale Verfahren eingesetzt, wie z. B. Modellprüfungswerkzeuge, mit deren Hilfe zu temporal-logischen Eigenschaften formalisierte Anforderungen nachgewiesen werden können. Aufgrund der hohen Komplexität heutiger Schaltungen können oftmals nur einzelne Komponenten verifiziert werden, jedoch nicht das gesamte System. Ein gängiger Ansatz, um die Anwendbarkeit formaler Verifikationsverfahren zu erhöhen, besteht in der Nutzung von Abstraktionstechniken, welche die Komplexität des zur Verifikation verwendeten Modells reduzieren. Es existieren verschiedene Abstraktionsverfahren, die häufig auf einer aufwendigen Neuberechnung des eingesetzten Modells beruhen. In der vorliegenden Dissertation wird ein alternativer Abstraktionsansatz vorgestellt. Ziel ist es, die formale Modellprüfung auf komplexere Systeme anzuwenden und Sicherheitseigenschaften des Systems zu verifizieren. Dazu wird in dieser Arbeit eine eigenschaftsbasierten Abstraktion für modular aufgebaute Systeme eingeführt, bei der die Komponenten des Systems mit Hilfe temporal-logischer Eigenschaften dargestellt werden. Insbesondere kann der Abstraktionsgrad dieser Darstellung leicht erhöht werden, indem eine unvollständige Eigenschaftsmenge zur Beschreibung einer Komponente verwendet wird. In diesem Fall ist das Verhalten der Komponenten durch die eingesetzten Eigenschaftsmengen nicht in allen Situationen eindeutig spezifiziert. Wenn bei der Verifikation einer Systemeigenschaft auf dem abstrakten Modell ein Gegenbeispiel ausgegeben wird, so muss überprüft werden, ob dieses auf dem konkreten System reproduzierbar ist. In der vorliegenden Arbeit wird eine automatisierte Analyse von Gegenbeispielen vorgestellt, welche prüft, ob ein Gegenbeispiel nur aufgrund von sogenannten Spezifikationslücken auftritt. Die Funktionalität der entwickelten Verfahren wird anhand von Beispielanwendungen gezeigt.