IC3 software model checking

Aachen (2018, 2019) [Buch, Doktorarbeit, Bericht]

Seite(n): 1 Online-Ressource (viii, 187 Seiten) : IllustrationenReport-Nummer: AIB-2019-02

Kurzfassung

In einer Zeit, in der Computer immer kleiner und leistungsfähiger und ihre Software immer komplexer wird und tiefer denn je unser tägliches Leben durchzieht, wachsen auch die Risiken von Fehlverhalten und die daraus resultierenden Schäden drastisch. Um solch ein unspezifiziertes Verhalten zu verhindern, hat sich das Model Checking, eine formale Verifikationstechnik zur Bestimmung funktionaler Eigenschaften von Informations- und Kommunikationssystemen, als besonders nützlich herausgestellt. Zum Beweis mathematischer Eigenschaften ist eine der ersten in den Schulen unterrichteten Methoden die Induktion. Mit ihrem Konzept, zunächst eine konkrete Induktionsbasis und anschließend einen abstrakten Induktionsschritt als Stellvertreter für beliebige Schritte zu beweisen, ist sie eine sehr einfache und intuitive, nichts desto trotz aber mächtige Beweistechnik. Dennoch kann es sehr schwierig sein eine induktive Formulierung für eine komplexe Eigenschaft zu finden. Wenn Menschen ein solches Problem zu lösen versuchen, erstellen sie intuitiv eine Menge kleinerer, einfacher Lemmata, welche zusammengenommen die gewünschte Eigenschaft implizieren. Jedes dieser Lemmata gilt relativ zu einer Teilmenge der vorher aufgestellten Lemmata und nutzt deren Wissen, um das neue Lemma zu beweisen. Dieser inkrementelle Ansatz, komplexe Eigenschaften mit Hilfe einer Menge kleiner, induktiver Lemmata zu beweisen, wurde für das Model Checking von Hardwaresystemen erstmals im IC3 Algorithmus angewendet und hat seitdem sämtliche existierenden Techniken zur Verifikation von Hardware geschlagen. Die vorliegende Arbeit zielt darauf ab, die von IC3 benutzen Methoden auf die Verifikation von Software für industrielle Steuerungsanlagen anzuwenden. Hierbei wird besonderes Augenmerk auf die Ausnutzung des vom Programm vorgegebenen Kontrollflusses gelegt. Zu diesem Zweck werden zunächst grundlegende Konzepte eingeführt und der IC3 Algorithmus mit seinen verschiedenen Phasen (Suchphase, Generalisierung und Propagation) im Detail erläutert. Auf dieser Grundlage wird der neue IC3CFA Algorithmus vorgestellt, welcher den Kontrollfluss explizit als Automaten modelliert, während die Variablenbelegungen symbolisch dargestellt werden, sodass die Vorteile aus beiden Welten vereint werden können. Nachfolgend wird die Leistungsfähigkeit des Algorithmus, sowie aller vorgestellten Verbesserungen ausführlich anhand eines anerkannten Satzes von Referenzprogrammen evaluiert. Um die erzielten Ergebnisse in einen Kontext zu setzen und die Leistungsfähigkeit des vorgestellten IC3CFA Algorithmus zu unterstreichen, schließt ein Vergleich zu anderen, bestehenden Implementierungen von IC3 Verifikationsalgorithmen für Software diese Arbeit ab.

Autorinnen und Autoren

Autorinnen und Autoren

Lange, Tim Felix

Gutachterinnen und Gutachter

Katoen, Joost-Pieter
Weissenbacher, Georg
Neuhäußer, Martin R.

Identifikationsnummern

  • REPORT NUMBER: RWTH-2019-01994

Downloads