Wir entwickeln Algorithmen, die dazu geeignet sind, Eigenschaften verteilter Systeme automatisch zu verifizieren. Im Mittelpunkt steht dabei die explizite Zustandsraumverifikation. Hier werden alle Zustände eines Systems explizit durchmustert, allerdings wegen des Problems der Zustandsexplosion nicht die Zustände des vorgegebenen Systems, sondern die eines daraus konstruierten, kleineren Systems. Solche Konstruktionstechniken nutzen z. B. die Symmetrie des Originalsystems oder die Tatsache, dass im Originalsystem viele Komponenten unabhängig voneinander arbeiten.
Ziel des Projektes ist es, die Liste verfügbarer Reduktionstechniken zu erweitern, existierende Techniken miteinander zu kombinieren, sowie effiziente Varianten existierender Techniken für spezielle Eigenschaftsklassen zu entwickeln. Im Zentrum dieses Projektes steht das Petrinetzbasierte Werkzeug LoLA.
Die begrenzende Ressource für computergestützte Verifikation ist im Gegensatz zu den meisten Problemen nicht die Laufzeit, sondern der Speicherplatz. Eine kostengünstige Möglichkeit zur Erweiterung des verfügbaren Speicherplatzes bietet die gemeinsame Nutzung vieler Rechner über ein lokales Netzwerk (z. B. Arbeitsplatzrechner außerhalb der Kernarbeitszeiten). Standardtechniken zur Bereitstellung eines physisch verteilten, virtuell gemeinsamen Speichers eignen sich leider nicht für Verifikationsalgorithmen. Daher suchen wir nach speziellen verteilten Verifikationsalgorithmen, die insbesondere den Überlauf und den Ausfall einiger beteiligter Rechner kompensieren.
Publikation: Karsten Wolf (Universität Rostock) : "Distributed Verification with LoLA".
Abstraktion ist das wichtigste Werkzeug zur Reduzierung des Zustandsraumes. Für einige Formalismen existieren bereits generische Abstraktionsalgorithmen. Die entstehenden Abstraktionen gestatten es, aus der Gültigkeit einer Eigenschaft im abstrakten System auf die Gültigkeit der Eigenschaft im originalen System zu schließen. Umgekehrt kann aber die Ungültigkeit der Eigenschaft im abstrakten System einerseits der Ungültigkeit im originalen System, andererseits aber auch einem zu hohen Abstraktionsgrad geschuldet sein. Da aber eine ungültige Eigenschaft immer mit einem Gegenbeispiel belegt wird, kann man durch die Analyse des Gegenbeispiels die Ursache für die Ungültigkeit ermitteln und ggf. die Abstraktion verfeinern.
Wir wollen diese Technologie im Kontext von High-Level-Petrinetzen erforschen, wo wir ein System dadurch abstrahieren, dass wir Farben (Daten) zu Klassen zusammenfassen und ununterscheidbar machen.
Seit einiger Zeit werden Techniken vorgeschlagen, mehr Speicher dadurch verfügbar zu machen, dass man einmal berechnete Zustände wieder löscht, wenn sie für die weitere Analyse nicht mehr benötigt werden. Eine dieser Techniken, die Sweep-Line-Methode, verwendet eine Progress-Measure um nicht mehr benötigte Zustände zu erkennen. Eine solche Measure kann man für Petrinetze automatisch berechnen. Die bisherige Berechnung lässt an mehreren Stellen nichtdeterministische Freiheitsgrade zu.
Wir wollen studieren, ob man diese Freiheitsgrade durch geeignete Heuristiken zur Steigerung der Leistungsfähigkeit nutzen kann.
Publikation: Karsten Wolf (Universität Rostock) : "Automated Generation of a Progress Measure for the Sweep-Line Method".
Es setzt sich die Erkenntnis durch, dass fast alle in der Praxis verwendeten mit temporaler Logik spezifizierten Eigenschaften eine sehr einfache logische Struktur haben. Meist werden nicht mehr als zwei Temporaloperatoren verwendet. Die Zahl solcher Eigenschaften beläuft sich auf reichlich 100.
Unser Ziel ist es, jede dieser Eigenschaften durch speziell darauf zugeschnittene Analyseverfahren, bzw. spezielle Varianten bekannter Reduktionstechniken gezielt zu unterstützen und damit die Leistungsfähigkeit allgemeiner Verifikationstechniken zu übertreffen.
Publikation: Karsten Wolf (Universität Rostock) : "Stubborn Sets for standard properties".
Als Vernetzung mit den Projekten zur Geschäftsprozessmodellierung am Lehrstuhl wollen wir Petrinetzmodelle verifizieren, die aus Modellen von Web Services, z. B. aus BPEL4WS oder WSCI generiert, entstehen. Aufgaben hier sind die gezielte Vereinfachung der aus automatischer Übersetzung entstehenden Modelle, die Erkennung von Engpässen in den existierenden Verifikationstechniken und deren Verbesserung (z. B. durch den Einsatz domainspezifischer Heuristiken).
Viele Modellierer verwenden gern Petrinetz-Elemente, die über die Standardelemente Stelle, Transition, Bogen, Marke hinausgehen. Eines dieser Konzepte sind die so genannten Reset-Kanten, die von einer Stelle so viele Marken abziehen wie sich dort befinden, unabhängig von deren Zahl. Für Resetkanten wurden in der Literatur bereits einige Analysetechniken vorgeschlagen.
Ziel ist die Sondierung der bekannten Techniken und deren Ergänzung, um die Funktionalität des Werkzeugs LoLA um das Behandeln von Resetkanten erweitern zu können.
In der expliziten Zustandsraumverifikation von Petrinetzen könnte Wissen über die Systemstruktur (Konflikte, Symmetrien, Siphons, Traps, Zustandsmaschinenkomponenten) hilfreich sein, deren Beschaffung oder Speicherung oft recht aufwändig ist.
Wir wollen die Frage klären, ob der Einsatz symbolischer Datenstrukturen (z. B. BDD) eine effiziente Berechnung und Verwaltung von Strukturinformationen gestattet.