Three-valued abstraction and heuristic-guided refinement for verifying concurrent systems

Diese Arbeit präsentiert ein abstraktionsverfeinerungsbasiertes Verifikationsframework für nebenläufige Systeme. Zur Abstraktion verwenden wir eine Kombination aus Prädikatabstraktion und Spotlightabstraktion. Dadurch werden zwei der Hauptursachen der Zustandskomplexität bei der Verifikation nebenläufiger Systeme angegangen. Eine weitere Besonderheit des Verfahrens ist der Einsatz einer 3-wertigen abstrakten Domäne. Eigenschaften in Systemmodellen können die Werte wahr, falsch und unbekannt annehmen, wodurch sich der abstraktionsbedingte Informationsverlust modellieren lässt: Alle wahr- und falsch-Resultate die sich bei der Verifikation ergeben, lassen sich auf das Originalsystem übertragen. Lediglich unbekannt-Resultate erfordern Verfeinerung. Dazu wird auf das Konzept der gegenbeispielgeleiteten Abstraktionsverfeinerung (CEGAR) zurückgegriffen. Gegenbeispiele sind unbekannte Fehlerpfade innerhalb eines Modells. Sie verweisen auf mögliche Verfeinerungsschritte zur Auflösung der Ungewissheit. Dies können neue Prädikate oder Prozesse sein. Typischerweise erweist sich nicht jeder potentielle Verfeinerungsschritt als zielführend, was die Auswahl geeigneter Schritte zu einer schwierigen Aufgabe macht. In dieser Arbeit wird eine Erweiterung des CEGAR-Konzepts eingeführt, basierend auf heuristischer Leitung: Auf Grundlage einer Abstraktionsabhängigkeitsanalyse werden potentielle Verfeinerungsschritte bezüglich des Nutzens für die aktuelle Verifikationsaufgabe heuristisch bewertet und der bestbewertete Schritt wird zur Verfeinerung ausgewählt. Wir zeigen, dass der heuristische Ansatz zu einer signifikanten Leistungssteigerung der Verifikation beitragen kann. Das entwickelte Verfahren erlaubt die Verifikation von CTL Eigenschaften von größenbeschränkten sowie parametrisierten nebenläufigen Systemen.In this thesis we introduce an abstraction refinement-based verification framework for concurrent systems. Our approach to abstraction is based on a combination of predicate abstraction, a data abstraction technique, and spotlight abstraction, a technique that abstracts away entire processes of a concurrent system. We thus tackle two major causes of state explosion in verification of concurrent systems. Another key feature of our approach is the use of a three-valued abstract domain. Properties in our system models can take the values true, false and unknown, which enables us to explicitly model the loss of information due to abstraction: All true and false results obtained via verification can be transferred to the original system, only unknown necessitates refinement. For refining the abstract models we follow the concept of counterexample-guided abstraction refinement (CEGAR). Counterexamples are unknown error paths in the model that typically hint at several possible ways to resolve the uncertainty via refinement. In our scenario, these refinement steps can involve the addition of new predicates or processes. However, not every potential refinement step is expedient, which makes the selection of an appropriate step exceedingly difficult. Therefore, we introduce an enhanced variant of CEGAR: Based on an abstraction dependence analysis the possible refinement steps, that we have derived from a counterexample, are heuristically evaluated with regard to their benefit for the current verification task, and the best evaluated step is chosen for refinement. We demonstrate that our heuristic approach can significantly improve the performance of abstraction-refinement-based verification. Our developed verification framework allows for reasoning about CTL properties of fixed-sized and parameterised concurrent systems.Tag der Verteidigung: 24.06.2013Paderborn, Univ., Diss., 201