Halbordnungs- und Reduktionstechniken für die automatische Verifikation von verteilten Systemen

Abstract

Das Hauptproblem bei der automatischen Verifikation von verteilten Systemen unter Verwendung von Model-Checking-Verfahren besteht in der Zustandsraumexplosion der Ausgangssysteme. Dieses bedeutet, daß sogar die Spezifikation eines kleinen Systems oftmals einen großen Zustandsraum aufspannt, da dieser exponentiell in der Größe des Ausgangssystems wachsen kann. In der Vergangenheit wurden verschiedene Techniken vorgeschlagen, um diese Problematik in den Griff zu bekommen. Diese können klassifiziert werden in Techniken, die auf eine implizite, kompakte Repräsentation des gesamten Zustandsraums abzielen, zum Beispiel codiert als BDD, oder die unter Verwendung von Abstraktionen oder Halbordnungsreduktionen eine reduzierte Zustandsraumrepräsentation verwenden. Eine dritte Klasse von Techniken stützt sich auf die Halbordnungssicht auf nebenläufige Berechnungen, und Systemzustände werden hier implizit durch die Verwendung azyklischer Petrinetze repräsentiert. Sehr populär darunter ist die Technik von McMillan zur Erzeugung endlicher, vollständiger Präfixe von Petrinetzentfaltungen. Das Ziel dieser Arbeit besteht darin, effiziente Halbordnungs- und Reduktionstechniken für die automatische Verifikation von verschiedenen Petrinetzklassen zu analysieren, zu erweitern, zu implementieren und experimentell zu vergleichen. Eine der Hauptfragestellungen auf dem Gebiet der automatischen Verifikation untersucht die Erreichbarkeit von Systemzuständen, da viele Sicherheitseigenschaften eines Systems auf einfache Erreichbarkeitsfragen zurückgeführt werden können. Als typisches Beispiel sei hier die Eigenschaft zum wechselseitigen Ausschluß von nebenläufigen Prozessen erwähnt. In dieser Arbeit werden vier Verfahren betrachtet, die das Erreichbarkeitsproblem für 1-sichere Petrinetze unter Verwendung von Entfaltungspräfixen exakt lösen. Es werden zwei Halbentscheidungsverfahren betrachtet, die das Erreichbarkeitsproblem für 1-sichere Petrinetze unter Verwendung von Techniken der linearen Programmierung zu lösen versuchen. Die Verfahren werden anhand von experimentellen Ergebnissen miteinander verglichen, und es wird eine Empfehlung hergeleitet, welche Verfahren für praktische Belange geeignet zu sein scheinen. Es wird gezeigt, daß das PSPACE-vollständige Erreichbarkeitsproblem für 1-sichere Petrinetze in ein (möglicherweise exponentiell größeres) NP-vollständiges Problem überführt werden kann, sofern Entfaltungstechniken eingesetzt werden. Eine weitere wichtige Fragestellung auf dem Gebiet der automatischen Verifikation beschäftigt sich mit dem Nachweis von Sicherheits- und Lebendigkeitseigenschaften, die in Form von temporalen Logiken wie beispielsweise CTL oder LTL formuliert werden. Es werden Reduktionsregeln für den Nachweis von LTL-X-Eigenschaften betrachtet, die in zwei Kategorien eingeteilt werden können: Regeln, die lineare Programmierung unter Verwendung von Invarianten oder impliziten Stellen einsetzen, und Regeln, die lokale Netzreduktionen betrachten. Es wird gezeigt, daß die Bedingungen für die Anwendbarkeit einiger lokaler Netzreduktionen abgeschwächt werden können, sofern man LTL-X-Eigenschaften mit einem Verfahren von Esparza und Heljanko nachweist. Anhand von experimentellen Ergebnissen wird gezeigt, daß die Verifikationszeit für eine LTL-X-Eigenschaft eines Systems signifikant verringert werden kann, sofern dieses mit den vorgeschlagenen Reduktionsregeln vorverarbeitet wird. Schließlich wird der von Esparza und Heljanko vorgestellte entfaltungsbasierte Ansatz zum Nachweis von LTL-X-Eigenschaften 1-sicherer Petrinetze auf eine höhere Petrinetzklasse übertragen. Anhand von experimentellen Ergebnissen wird der in dieser Arbeit vorgestellte Ansatz mit dem Ansatz von Esparza und Heljanko sowie dem Model-Checker SPIN verglichen. Die Ergebnisse zeigen, daß der in dieser Arbeit verwendete Model-Checker dem Model-Checker von Esparza und Heljanko in allen Beispielen, und SPIN gegenüber in einigen Beispielen überlegen ist.

The main problem in automatic verification of distributed systems using model checking techniques is that it suffers from state space explosion. This means that even a relatively small system specification often yields a very large state space that may grow exponentially in the size of the original system. Many different techniques have been proposed to alleviate this problem. They can be classified into techniques that aim at an implicit compact representation of the full state space, for instance coded as a BDD, or at an explicit generation of a reduced state space presentation using abstraction or partial-order reduction techniques. A third class of techniques relies on the partial-order view of concurrent computation, and represents system states implicitly using acyclic Petri nets. Among them, McMillan's finite complete prefixes of Petri net unfoldings are a very popular technique. The goal of this work is to analyse, to improve, to implement, and to compare efficient partial-order and Petri net reduction techniques for model checking tasks regarding different classes of Petri nets. One of the key questions in the area of automatic verification is the reachability of states because many safety properties of systems can be reduced to simple reachability properties. A typical example is the mutual-exclusion property of mutual-exclusion algorithms. This work studies four solutions to the reachability problem for 1-safe Petri nets that are based on the unfolding technique. Two semi-decision algorithms are presented that try to solve the reachability problem for 1-safe Petri nets without unfoldings but with linear programming techniques. All algorithms are tested on a set of examples and a recommendation is extracted on which algorithms should be used and which ones not. It is shown that the PSPACE-complete reachability problem for 1-safe Petri nets can be translated into a (probably exponentially larger) NP-complete problem using Petri net unfoldings. Another important task in the area of automatic verification is the verification of safety and liveness properties which are expressed in terms of temporal logics like CTL and LTL. A set of reduction rules for LTL-X model checking of 1-safe Petri nets is presented. The reduction techniques are of two kinds: Linear programming techniques based on Petri net techniques like invariants and implicit places, and local net reductions. It is shown that the conditions for the application of some local net reductions can be weakened using an LTL-X model checking approach which has been proposed by Esparza and Heljanko. A number of experimental results is presented, and it is shown that the model checking time of a net system can be significantly decreased if it has been preprocessed with the proposed reduction techniques. Finally, the unfolding-based approach to LTL-X model checking of 1-safe Petri nets proposed by Esparza and Heljanko is extended to high-level Petri nets. A number of experimental results is presented comparing the approach of this thesis with the one proposed by Esparza and Heljanko and the well-known model checker SPIN, and it is shown that the model checker presented in this thesis beats the one of Esparza and Heljanko on all examples, and has the edge over SPIN in some examples.