Compositional Verification of Concurrent Softwaremodels with Model Checking

Die größte praktische Einschränkung für Model Checking ist in dem Zustandsexplosionsproblem zu sehen. Aus diesem Grund sind verschiedene Veröffentlichungen entstanden, in denen das Zustandsexplosionsproblem durch symbolische Speichertechniken, Abstraktionen oder Halbordnungsreduktionen abgeschwächt wird. Kompositionale Verifikationsmethoden erzeugen hierbei einen besonders effizienten Ansatz, bei dem der globale Verifikationsaufwand auf die lokalen Komponenten verlagert wird; die Gültigkeit der globalen Prüfbedingung wird dann durch Komposition der lokal verifizierten Teilbedingungen gesichert. Obwohl kompositionale Verifikationsmethoden das Zustandsexplosionsproblem vermeiden, ist der praktische Einsatz durch die zeitaufwändige Dekomposition der globalen Spezifikation in lokale Teilformeln eingeschränkt. In dieser Arbeit beschreiben wir eine neue kompositionale Verifikationstechnik, die die Lücke zwischen der vollautomatischen Verifikation durch Model Checking und den sehr effizienten kompositionalen Verifikationsmethoden schließt. Die Dekomposition globaler Prüfbedingungen in lokale Bedingungen wird mithilfe eines Algorithmus vorgenommen, während die lokale Verifikation durch Model Checking möglich ist. Damit beschreiben wir ein vollständig automatisches kompositionales Verifikationsverfahren. Das Verfahren wird anhand eines industriellen Beispiels hoher Komplexität evaluiert.Dealing with Model Checking, the state explosion problem is often referred to as the main restriction for practical use. Thus, there are various publications trying to weaken the state explosion problem by using symbolic model descriptions, abstractions or partial order reduction techniques. A very efficient way comes along with the compositional verification approach by shifting the global verification amount to its local components; then, the global properties are established by composing the locally verified component properties. Although compositional verification approaches are able to avoid the state explosion problem, practical use is restricted by tedious decomposition of global specifications into its local parts. In this thesis we describe a novel compositional verification technique which bridges the gap between fully automatic verification done by model checking and very efficient compositional verification approaches. We give an algorithmic description for decomposing global proof-conditions and show how these local conditions can be verified by model checking. Thus, we describe a fully automatic compositional verification technique. The overall approach is evaluated with an industrial example of a non toy complexity