Zugl.: Paderborn, Univ., Diss., 2008

Paderborn, Universiẗat, Diss., 2008.

We present an extension of the popular probabilistic model checker PRISM with multi-actions that enables the modeling of complex coordination between stochastic components in an exogenous manner. This is supported by tooling that allows the use of the exogenous coordination language Reo for specifying the coordination glue code. The tool provides an automatic compilation feature for translating a Reo network of channels into PRISM's guarded command language. Additionally, the tool supports the translation of reward monitoring components that can be attached to the Reo network to assign rewards or cost to activity within the coordination network. The semantics of the translated model is then based on weighted Markov decision processes that yield the basis, e.g., for a quantitative analysis using PRISM. Feasibility of the approach is shown by a quantitative analysis of an energy-aware network system example modeled with a role-based modeling approach in Reo.

Beim Austausch von Intellectual Properties (IP) entsteht das Problem, daß der Anwender oftmals nicht sicher feststellen kann, ob die gewünschte Parameterkombination unterstützt wird bzw. ob die IP mit den gewünschten Einstellungen korrekt arbeitet. Ziel dieser Arbeit ist es, eine mögliche Lösung zur Parameterprüfung bereitzustellen. Im Rahmen des vom Bundesministerium für Bildung und Forschung (BMBF) geförderten Projekts Intellectual Property Qualifikation für effizientes Systemdesign [IPQ] wurde dazu das Entwurfswerkzeug entwickelt. Anhand einer durch den Entwerfer vorgegebenen formalen Beschreibung der Parameter und ihrer Abhängigkeiten untereinander prüft eine vom Werkzeug automatisch generierte Testbenchkomponente, ob alle Bedingungen eingehalten werden. Des weiteren berechnet diese Komponente auf der Basis vorgegebener Gleichungen verschiedene Systemeigenschaften, wie beispielsweise die maximale Taktfrequenzabweichung zwischen Sender und Empfänger einer seriellen Übertragungsstrecke. Diese können dann vom Anwender mit der ihm vorliegenden Spezifikation verglichen werden. ist außerdem in der Lage, anhand der Parameterabhängigkeiten die verschiedenen Kombinationen von Einstellungen zu berechnen, die nötig sind, um den kompletten Parameterraum abzudecken, und diese in Form eines Parameter-Domänen-Graphen darzustellen. Mit Hilfe dieses Graphen ist der Anwender in der Lage, Kombinationen gezielt so auszuwählen, daß ein möglichst hoher Verifikationsgrad der IP erreicht wird, ohne unnötig viele Simulationen durchführen zu müssen.

Die modellgetriebene Entwicklung (MDD) ist ein Ansatz, um formale Modelle automatisiert in ausführbare Software zu übersetzen. Obwohl dieses Vorgehen die Häufigkeit von Fehlern im generierten Quellcode verringert, können immer noch die Ausgangsmodelle fehlerhaft sein. Deshalb sind zusätzliche Prüfverfahren, wie z.B. die Verwendung eines Model Checkers sinnvoll. Er stellt automatisiert sicher, dass ein Modell alle gestellten Anforderungen erfüllt. Das Ziel dieser Arbeit ist daher die Integration eines Model Checkers in den modellgetriebenen Entwicklungsprozess, um die Qualität von Software-Produkten zu verbessern. Zu diesem Zweck wird das sogenannte DSL Verification Framework (DVF) vorgestellt. Es stellt Entwicklern vorgefertigte Sprachkonstrukte zur Verfügung, um die Implementierung von Parsern und Transformatoren zu erleichtern. Des Weiteren berücksichtigt es auch die "State Space Explosion", damit auch größere Modelle verifizierbar bleiben. Um die praktische Nutzung des DVF zu evaluieren, werden zwei Industriefallstudien durchgeführt.

A knowledge-based program defines the behavior of an agent by combining primitive actions, programming constructs and test conditions that make explicit reference to the agent’s knowledge. In this paper we consider a setting where an agent is equipped with a Description Logic (DL) knowledge base providing general domain knowledge and an incomplete description of the initial situation. We introduce a corresponding new DL-based action language that allows for representing both physical and sensing actions, and that we then use to build knowledge-based programs with test conditions expressed in the epistemic DL. After proving undecidability for the general case, we then discuss a restricted fragment where verification becomes decidable. The provided proof is constructive and comes with an upper bound on the procedure’s complexity.

The meet up between data, processes and structural knowledge in modeling complex enterprise systems is a challenging task that has led to the study of combining formalisms from knowledge representation, database theory, and process management. Moreover, to ensure system correctness, formal verification also comes into play as a promising approach that offers well-established techniques. In line with this, significant results have been obtained within the research on data-aware business processes, which studies the marriage between static and dynamic aspects of a system within a unified framework. However, several limitations are still present. Various formalisms for data-aware processes that have been studied typically use a simple mechanism for specifying the system dynamics. The majority of works also assume a rather simple treatment of inconsistency (i.e., reject inconsistent system states). Many researches in this area that consider structural domain knowledge typically also assume that such knowledge remains fixed along the system evolution (context-independent), and this might be too restrictive. Moreover, the information model of data-aware processes sometimes relies on relatively simple structures. This situation might cause an abstraction gap between the high-level conceptual view that business stakeholders have, and the low-level representation of information. When it comes to verification, taking into account all of the aspects above makes the problem more challenging. In this thesis, we investigate the verification of data-aware processes in the presence of ontologies while at the same time addressing all limitations above. Specifically, we provide the following contributions: (1) We propose a formal framework called Golog-KABs (GKABs), by leveraging on the state of the art formalisms for data-aware processes equipped with ontologies. GKABs enable us to specify semantically-rich data-aware business processes, where the system dynamics are specified using a high-level action language inspired by the Golog programming language. (2) We propose a parametric execution semantics for GKABs that is able to elegantly accommodate a plethora of inconsistency-aware semantics based on the well-known notion of repair, and this leads us to consider several variants of inconsistency-aware GKABs. (3) We enhance GKABs towards context-sensitive GKABs that take into account the contextual information during the system evolution. (4) We marry these two settings and introduce inconsistency-aware context-sensitive GKABs. (5) We introduce the so-called Alternating-GKABs that allow for a more fine-grained analysis over the evolution of inconsistency-aware context-sensitive systems. (6) In addition to GKABs, we introduce a novel framework called Semantically-Enhanced Data-Aware Processes (SEDAPs) that, by utilizing ontologies, enable us to have a high-level conceptual view over the evolution of the underlying system. We provide not only theoretical results, but have also implemented this concept of SEDAPs. We also provide numerous reductions for the verification of sophisticated first-order temporal properties over all of the settings above, and show that verification can be addressed using existing techniques developed for Data-Centric Dynamic Systems (which is a well-established data-aware processes framework), under suitable boundedness assumptions for the number of objects freshly introduced in the system while it evolves. Notably, all proposed GKAB extensions have no negative impact on computational complexity.

In dieser Arbeit geht es um die schrittweise Verfeinerung verteilter Algorithmen. Dabei wird ein einfacher Algorithmus, der einige gewünschte Eigenschaften hat, Schritt für Schritt zu einem komplexen Algorithmus verfeinert, der konkrete Implementationsanforderungen erfüllt, so daß in jedem Schritt die gewünschten Eigenschaften erhalten bleiben. Wir stellen einen neuen eigenschaftserhaltenden Verfeinerungsbegriff vor, der auf der kausalen Ordnung der Aktionen eines Algorithmus basiert. Diesen Begriff definieren wir als Transitionsverfeinerung für elementare Petrinetze und diskutieren Beweiskriterien. Danach definieren und diskutieren wir die simultane Verfeinerung mehrerer Transitionen. Zur Modellierung komplexer verteilter Algorithmen sind elementare Petrinetze oft nicht adäquat. Wir benutzen deshalb algebraische Petrinetze. Wir definieren Transitionsverfeinerung für algebraische Petrinetze und stellen einen Zusammenhang zur simultanen Verfeinerung von Transitionen in elementaren Petrinetzen her. Transitionsverfeinerung ist besonders für Verfeinerungsschritte geeignet, in denen synchrone Kommunikation zwischen Agenten durch asynchronen Nachrichtenaustausch ersetzt wird. Wir zeigen dies am Beispiel eines komplexen verteilten Algorithmus, zur Berechnung des minimalen spannenden Baumes in einem gewichteten Graphen. Wir zeigen die Korrektheit dieses Algorithmus in mehreren Schritten, von denen einige Schritte Transitionsverfeinerungen sind. In anderen Schritten sind klassische Verfeinerungsbegriffe ausreichend. Wir übertragen deshalb auch einen klassischen Verfeinerungsbegriff in unser formales Modell. / The topic of this PhD thesis is the stepwise refinement of distributed algorithms. Stepwise refinement starts with a simple algorithm with certain desired properties. This algorithm is refined step by step such that the desired properties are preserved in each refinement step. The result is a complex distributed algorithm which satisfies concrete implementation requirements and which still has the desired properties. We propose a new property preserving notion of refinement which is based on the causal ordering of actions of an algorithm. We call this notion transition refinement and we define it first for elementary Petri nets. Furthermore, we discuss proof criteria. Then, we define and discuss the simultaneous refinement of several transitions. For modelling complex distributed algorithms, we use algebraic Petri nets instead of elementary Petri nets. We define transition refinement for algebraic Petri nets, and we show its relationship to simultaneous transition refinement in elementary Petri nets. Transition refinement is particularly suitable for refinement steps in which synchronous communication between agents is replaced by asynchronous message passing. We show this by means of a complex distributed algorithm for determining the minimal spanning tree of a weighted graph. We prove the correctness of this algorithm in several steps. Some of these steps are transition refinements. For other steps, well-known notions of refinement are sufficient. Therefore, we also carry over a well-known notion of refinement into our formal model.

Gegenstand der Arbeit ist die Verifikation von verteilten diskreten Systemen in bezug auf Spezifikationen ihres Verhaltens. Diskrete Systeme bestehen aus einer abzaehlbaren Zustandsmenge und einer Zustandsuebergangsrelation. Bei verteilten Systemen ist eine signifikante Zahl von Zustandsuebergaengen nur durch eine kleine Zahl von Komponenten eines strukturierten Zustandsraumes bedingt und aendert auch nur wenige Komponenten. Bei praktisch relevanten Systemen ist die Zustandszahl unbeherrschbar gross. Dieses Phaenomen wird Zustandsraumexplosion genannt. Verteiltheit gilt als eine der wesentlichen Ursachen fuer Zustandsraumexplosion, weil nebenlaeufig moegliche lokale Zustandsuebergaenge abhaengig von ihren exponentiell vielen Ausfuehrungsreihenfolgen exponentiell viele verschiedene Zwischenzustaende erzeugen koennen. Fuer Verifikationsaufgaben sind Systeme daher implizit gegeben durch eine Beschreibung von Anfangszustaenden und (lokale) Regeln zur Generierung von Folgezustaenden. Solche Systembeschreibungen folgen verschiedenen Paradigmen, z.B. dem variablenorientierten Paradigma (Zustaende sind Werte von Variablen, die durch Zustandsuebergaenge gelesen und geschrieben werden) oder dem ressourcenorientierten Paradigma (Zustaende sind Verteilungen von Ressourcen im System, die durch Zustandsuebergaenge konsumiert oder produziert werden). Die Verfuegbarkeit von Verifikationstechniken oder spezifischen Implementationen haengt vom zugrundeliegenden Paradigma ab. Als Sprache zur Formulierung von Spezifikationen des Verhaltens verwenden wir etablierte temporale Logiken und fuer die Praxis bedeutsame Fragmente solcher Logiken. Temporale Logik beschreibt Eigenschaften von Abfolgen von Zustaenden, basierend auf elementaren, einzelne Zustaende betreffenden Eigenschaften. Auf einer expliziten Systemdarstellung lassen sich temporallogische Eigenschaften effizient, d.h. mit einer linear von der Zustandszahl abhaengigen Laufzeit, verifizieren. Eine solche Verifikation basiert auf einfachen Suchalgorithmen in dem durch das System definierten Zustandsgraph. Ein solcher Verifikationsansatz ist aber wegen der genannten Zustandsraumexplosion nicht durchfuehrbar. Im wesentlichen werden drei Loesungsansaetze in Richtung durchfuehrbarer Verifikationsalgorithmen verfolgt. Die strukturelle Verifikation versucht, Eigenschaften direkt aus spezifischen Mustern in der impliziten Systembeschreibung abzuleiten. Der derzeitige Stand der Technik gestattet solche Ableitungen nur fuer wenige und einfach strukturierte Verhaltensspezifikationen und erfordert auch dann in einigen Faellen recht aufwendige Berechnungen. Bei der symbolischen Zustandsraumanalyse wird der Zustandsraum erschoepfend durchmustert, allerdings unter Benutzung von Datenstrukturen, deren elementare Objekte ganze Mengen von Zustaenden beschreiben, und deren elementare Operationen die Folgezustaende fuer ganze solche Mengen aus der impliziten Systembeschreibung errechnen. Bei der expliziten Zustandsraumverifikation, dem Thema der vorliegenden Habilitationsschrift, wird eine explizite Repraesentation eines Zustandsraumes generiert, der wesentlich kleiner ist als der Zustandsraum des untersuchten Systems, in bezug auf die untersuchte Eigenschaft aber per Konstruktion aequivalent zum originalen System ist. Zur Konstruktion werden Informationen aus der impliziten Systembeschreibung herangezogen. Eine Technologie zur expliziten Zustandsraumverifikation besteht also aus - Einer mathematisch fundierten Theorie, die einer bestimmten Konstruktionsmethode bescheinigt, welche Eigenschaften durch sie bewahrt werden; - effizienten Algorithmen zur Implementation eine solchen Konstruktion; Die Arbeit enthaelt, fuer mehrere bekannte Verfahren, Beitraege zu jeweils mindestens einem der beiden Bestandteile einer expliziten Zustandsraumverifikationstechnik. Die Methode der sturen Mengen verkleinert den explizit zu konstruierenden Zustandsraum dadurch, dass von den in einem Zustand moeglichen Zustandsuebergaengen nur einige tatsaechlich untersucht werden, so dass weit weniger Zwischenzustaende durch verschiedene Abfolge nebenlaeufiger lokaler Zustandsuebergaenge entstehen. Die zu untersuchenden Uebergaenge werden abhaengig von der zu verifizierenden Eigenschaft und Informationen aus der Systemstruktur so ausgewaehlt, dass zu jeder Klasse von fuer die Eigenschaft relevanten Systemablaeufen wenigstens einer im reduzierten Zustandsraum repraesentiert ist. Die erste 1988 veroeffentlichte Methode diente der Bewahrung von terminalen Zustaenden sowie mindestens eines Pfades unendlicher Laenge. In der Folge wurde diese Technik auf viele andere Klassen von Eigenschaften erweitert, wobei vor allem die Faehigkeit, einen unendlichen Pfad zu bewahren, dahingehend verfeinert wurde, dass gezielt Pfade mit bestimmten Eigenschaften bewahrt werden konnten. Dabei spielte das Konzept unsichtbarer Zustandsuebergaenge eine tragende Rolle, wobei ein unsichtbarer Zustandsuebergang die Eigenschaft hat, dass er keine fuer die Eigenschaft relevanten Zustandskomponenten aendert. Daher war die Anwendung der Methode sturer Mengen begrenzt auf lokale Systemeigenschaften, weil andereseits zu wenige unsichtbare Uebergaenge fuer eine substantielle Reduktion zur Verfuegung stuenden. In der vorliegenden Arbeit setzen wir an der ersten Arbeit zur Methode sturer Mengen an und verfeinern die Faehigkeit, terminale Zustaende zu bewahren, dahingehend, dass nun die Praesenz von Zustaenden mit beliebigen in temporaler Logik formulierbaren Eigenschaften bewahrt werden. Die neue Methode basiert nicht auf der Existenz unsichtbarer Uebergaenge und kann in der Tat auch bei der Verifikation globaler Systemeigenschaften zu substantieller Reduktion fuehren. Das neue Konzept zur Konstruktion des reduzierten Zustandsraumes sind sogenannte UP-Mengen. Eine UP-Menge ist eine Menge von Uebergaengen, von denen mindestens einer in einem Systemablauf von einem Zustand, der die untersuchte Eigenschaft nicht erfuellt, zu einem Zustand, der die Eigenschaft erfuellt, vorkommen muss. Wir geben Algorithmen an, die kleine UP-Mengen fuer beliebige Zustaende aus der impliziten Systembeschreibung und einer Repraesentation der untersuchten Eigenschaft in der temporalen Logik CTL berechnet. Wir zeigen, dass jede Konstruktion, die in einem Zustand alle Uebergaenge in einer schwach sturen Obermenge einer zu dem Zustand berechneten UP-Menge untersucht, alle Zustaende erreicht, die die Eigenschaft besitzen. Dabei ist die Konstruktion schwach sturer Mengen die allen Methoden sturer Mengen gemeinsame Grundkonstruktion. Symmetrische Reduktion verkleinert den zu untersuchenden Zustandsraum dadurch, dass zu jeder Klasse von in bezug auf Symmetrie aequivalenten Zustaenden jeweils nur einer weiterverfolgt wird. Dadurch lassen sich alle gegenueber Symmetrie insensitive Eigenschaften bewahren (wobei man oft Insensitivitaet einer Eigenschaft durch die geeignete Wahl der Symmetrienmenge erreichen kann). Symmetrische Reduktion beinhaltet zwei Probleme, erstens das Aufinden der einem System innewohnenden Symmetrie, und zweitens, zu einem gegebenen Zustand, das Auffinden zu ihm aequivalenter Zustaende in der Menge bereits untersuchter Zustaende. Die meisten vorhandenen Implementationen leiten Symmetrien aus speziellen Datenstrukturen ab, in denen wegen der eingeschraenkten Operationen die verschiedenen Elemente des Typs austauschbar sind. Das Auffinden aequivalenter Zustaende wird durch eine Transformation neu berechnter Zustaende in einen aequivalenten kanonischen Repraesentanten realisert. Alternativ zu diesem Ansatz wurde zur Beschreibung von Symmetrien die Verwendung von Graphautomorphismen auf netzartigen impliziten Systembeschreibungsformen vorgeschlagen. Es zeigt sich, dass per Umwandlung von Datenabhaengigkeiten in Graphrepraesentationen, jede Datentypsymmetrie auch einen Graphautomorphismus bildet, andererseits aber durch Graphautomorphismen Symmetrien beschreibbar sind, die sich in Datentypbetrachtungen nicht wiederfinden lassen. Diese zusaetzlichen Symmetrien erlauben eine staerkere Reduktion des Zustandsraumes. Zur Graphautomorphismentechnik fehlten bislang leistungsfaehige Algorithmen zur Umsetzung dieser Technologie. Wir setzen an der auf Graphautomorphismen basierenden Methode an und unterlegen alle Teilprobleme mit leistungsfaehigen Algorithmen. Die Berechnung der Automorphismen beschraenken wir auf ein Erzeugendensystem, das polynomiell viele Elemente, gemessen an der Groesse der impliziten Systembeschreibung, hat. Die Berechnung selbst ist schlimmstenfalls exponentiell, was nicht verwundert, weil das Problem mit einem Entscheidungsproblem eng korreliert, von dem bekannt ist, dass es in der Klasse NP, aber unbekannt, ob es NP-vollstaendig oder in P liegt. Diese Eigenschaft hat dem Problem eingehende Untersuchung zuteil werden lassen, wegen der nach wie vor offenen "P ungleich NP?"-Frage. Trotzdem ist kein polynomieller Algorithmus bekannt. Umso erfreulicher ist es, dass unser Berechnungsalgorithmus sich auf realistischen Beispielen bisher durchweg polynomiell verhielt, und lediglich bei eigens konstruierten Systemen ins Exponentielle ausriss. Fuer die Loesung des Problems, aequivalente bereits bekannte Zustaende aufzuspueren, schlagen wir mehrere Techniken vor und beschreiben ihre Leistungsfaehigkeit abhaengig von der Struktur der innewohnenden Symmetrie. Fuer duenne Symmetriegruppen (wenige symmetrische Transformationen) eignet sich eine Technik, bei der die Symmetrien der Reihe nach aus dem Erzeugendensystem generiert werden, und das symmetrische Bild des neuen Zustandes mit der Menge der bekannten Zustaende verglichen wird. Dabei koennen wir, abhaengig vom Ausgang einer solchen Ueberpruefung, die Generierung von Symmetrien unterdruecken, von denen aus vorhandenen Informationen klar ist, dass sie keinesfalls zum Erfolg fuehren. Dadurch kann eine erhebliche Effizienzsteigerung erzielt werden. Bei einer zweiten Technik iterieren wir die bekannten Zustaende, genauer gesagt, diejenigen Zustaende, die fuer eine die Symmetrie respektierende Hashfunktion denselben Wert liefert wie der neue Zustand, ob es eine Symmetrie gibt, die beide Zustaende ineinander ueberfuehrt. Das verbleibende Problem kann durch eine Adaption des Symmetrieberechnungsverfahrens geloest werden. Eine vorherige Berechnung des Erzeugendensystems kann entfallen. Die dritte vorgeschlagene Technik benutzt das Erzeugendensystem, um den neuen Zustand approximativ in einen kanonischen aequivalenten Zustand zu ueberfuehren. Diese Technik ist von allen beschriebenen Methoden die effizienteste, liefert aber groessere Zustandsraeume als die beiden anderen Techniken. Wir studieren die Vor- und Nachteile aller Techniken anhand mehrerer Beispielsysteme. Die dritte in der Arbeit behandelte Technik ist die Methode der Ueberdeckbarkeitsgraphen. Sie ist spezifisch fuer die ressourcenbasierte Systembeschreibungsform der Petrinetze. Sie diente urspruenglich zur Aufspuerung von Stellen im System, an denen sich unbeschraenkt viele Ressourcen ansammeln koennen. Formal ist ein Ueberdeckbarkeitsgraph eine endliche Abstraktion eines Systems mit bis zu unendlich vielen Zustaenden. Von nur wenigen Eigenschaften war bekannt, dass sie sich aus dem Ueberdeckbarkeitsgraphen ableiten lassen. Wir formulieren Regeln zur Auswertung von Ueberdeckbarkeitsgraphen, mit deren Hilfe es moeglich ist, eine Vielzahl von in temporaler Logik formulierten Eigenschaften aus dem Ueberdeckbarkeitsgraph abzuleiten. Diese Reglen sind inhaerent unvollstaendig, da bekannt ist, dass fuer viele Eigenschaften es Paare von Systemen gibt, die isomorphe Ueberdeckbarkeitsgraphen liefern, sich aber in bezug auf die Eigenschaft verschieden verhalten. Fuer universelle Eigenschaften des CTL-Fragments ACTL erhalten wir Bewahrungsresultate durch das Ausweisen einer Simulationsrelation zwischen dem originalen System und seinem Ueberdeckbarkeitsgraph. Fuer existentielle Eigenschaften basieren unsere Resultate auf einer Abschwaechung der Erfuellbarkeitsrelation ueber Zustaenden des Ueberdeckbarkeitsgraphen. Einem Zustand des Ueberdeckbarkeitsgraphen entsprechen divergierende Folgen von Zustaenden des Originalgraphen. Normalerweise schreibt man einem Zustand des Ueberdeckbarkeitsgraphen dann eine Eigenschaft zu, wenn alle Folgenglieder im Originalsystem die Eigenschaft besitzen. Wir arbeiten dagegen mit einem Begriff, wo Gueltigkeit der Eigenschaft nur fuer fast alle Folgenglieder gefordert wird. Eine letzte Gruppe von Techniken ist bisher in der Zustandsraumverifikation nicht eingestzt worden, aber aus der strukturellen Verifikation fuer Petrinetze bekannt. Zu einem Petrinetz kann eine ganzzahlige Inzidenzmatrix C gebildet werden, mit deren Hilfe ein linear-algebraischer Zusammenhang zwischen voneinander errichbaren Zustaenden hergestellt werden kann. Stellen- und Transitionsinvarianten sind Loesungen der durch C-T bzw. C definierten homogenen Gleichungssysteme. Dabei dienen Stelleninvarianten gewoehnlich einer Abschaetzung der Menge der erreichbaren Zustaende nach oben, mit daraus resultierenden Moeglichkeiten der Ableitung von Eigenschaften, waehrend Transitionsinvarianten Zyklen im Zustandsraum charakterisieren. Wir verwenden Stelleninvarianten zur Kompression von einzelnen Zustaenden. Durch Stelleninvarianten lassen sich einige Komponenten in einen funktionalen Zusammenhang zu den verbleibenden Komponenten stellen. Dadurch ist auch nach dem Streichen der funktional abhaengigen Stellen der Zustand noch eindeutig determiniert. Wir zeigen, dass bei der Konstruktion des Zustandsraumes ein durch die verbleibenden Stellen gebildeter "Fingerabdruck" ausreicht. Transitionsinvarianten verwenden wir dazu, eine Menge von Zustaenden so auszuzeichnen, dass jeder Zyklus im Zustandsraum mindestens einen ausgezeichneten Zustand enthaelt. Darufhin speichern wir noch noch ausgezeichnete Zustaende permanent, sparen also Speicherplatz. Fuer nicht ausgezeichnete Zustaende kann es passieren, dass sie mehrmals aufgesucht werden (auf verschiedene Weise aus Vorgaengerzustaenden entstehen). Weil sie nicht gespeichert sind, werden auch wiederholt ihre Nachfolgezustaende untersucht. Da in jedem Kreis mindestens ein ausgezeichneter, also permanent zu speichernder Zustand enthalten ist, entstehen durch diese wiederholte Berechnung keine Probleme in bezug auf Terminierung des Verfahrens, wohl aber erhebliche Laufzeiteinbussen. Wir schlagen Methoden zur Begrenzung der Laufzeiteinbussen um den Preis weiterer zu speichernder Zustaende vor. Fuer alle untersuchten Methoden studieren wir die Abhaengigkeit der Anwendbarkeit und Effizienz der Methode von dem der gegebenen impliziten Systembeschreibung zugrundeliegenden Paradigma. Wir untersuchen ebenfalls die Kompatibilitaet der Verfahren mit verschiedenen Strategien zur Generierung des Zustandsraumes (Tiefe zuerst, Breite zuerst, verteilt) und Moeglichkeiten der gemeinsamen Anwendung verschiedener Techniken. / Verification is the task of determining whether a (model of a) system holds a given behavioral property. State space verification comprises a class of computer aided verification techniques where the property is verified through exhaustive exploration of the reachable states of the system. Brute force implementations of state space verification are intractable, due to the well known state explosion problem. Explicit state space verification techniques explore the state space one state at a time, and rely usually on data structures where the size of the data structure increases monotonously with an increasing number of explored states. They alleviate state explosion by constructing a reduced state space that, by a mathematically founded construction, behaves like the original system with respect to the specified properties. Thereby, decrease of the number of states in the reduced system is the core issue of a reduction technique thus reducing the amount of memory required. An explicit state space verification technique comprises of - a theory that establishes whether, and how, certain properties can be preserved through a construction of a reduced state space; - a set of procedures to execute the actual construction efficiently. In this thesis, we contribute to several existing explicit state space verification techniques in either of these two respects. We extend the class of stubborn set methods (an instance of partial order reduction) by constructions that preserve previously unsupported classes of properties. Many existing constructions rely on the existence of "invisible" actions, i.e. actions whose effect does not immediately influence the verified property. We propose efficient constructions that can be applied without having such invisible actions, and prove that they preserve reachability properties as well as certain classes of more complex behavioral system properties. This way, so called "global" properties can now be approached with better stubborn set methods. We pick up a graph automorphism based approach to symmetry reduction and propose a set of construction algorithms that make this approach feasible. In difference to established symmetry techniques that rely on special "symmetry creating" data types, a broader range of symmetries can be handled with our approach thus obtaining smaller reduced state spaces. Coverability graph construction leads to a finite representation of an infinite state space of a Petri net by condensing diverging sequences of states to their limit. We prove rules to determine temporal logic properties of the original system from its coverability graph, far beyond the few properties known to be preserved so far. We employ the Petri net concept of linear algebraic invariants for compressing states as well as for leaving states out of explicit storage. Compression uses place invariants for replacing states by smaller fingerprints that still uniquely identify a state (unlike many hash compression techniques). For reducing the number of explicitly stored states, we rely on the capability of Petri net transition invariants to characterize cycles in the state space. For termination of an exhaustive exploration of a finite state space, it is sufficient to cover all cycles with explicitly stored states. Both techniques are easy consequences of well known facts about invariants. As a novel contribution, we observe that both techniques can be applied without computing an explicit representation of (a generating set for) the respective invariants. This speeds up the constructions considerably and saves a significant amount of memory. For all presented techniques, we illustrate their capabilities to reduce the complexity of state space reduction using a few academic benchmark examples. We address compatibility issues, i.e. the possibility to apply techniques in combination, or in connection with different strategies for exploring the reduced state space. We propose a scheme to distribute state space exploration on a cluster of workstations and discuss consequences for using this scheme for state space reduction. We collect observations concerning the impact of the choice of system description formalisms, and property specification languages, on the availability of explicit state space verification techniques.

Chipkarten sind ein fester Bestandteil unseres täglichen Lebens, das immer stärker von der Zuverlässigkeit derartiger Sicherheitssysteme abhängt, zum Beispiel Bezahlkarten, elektronische Gesundheitskarten oder Ausweisdokumente. Eine Sicherheitspolitik beschreibt die wichtigsten Sicherheitsziele und Sicherheitsfunktionen eines Systems und bildet die Grundlage für dessen zuverlässige Entwicklung. In der Arbeit konzentrieren wir uns auf multi-applikative Chipkartenbetriebssysteme und betrachten neue zusätzliche Sicherheitsziele, die dem Schutz der Kartenanwendungen dienen. Da die Qualität des Betriebssystems von der umgesetzten Sicherheitspolitik abhängt, ist deren Korrektheit von entscheidender Bedeutung. Mit einer Formalisierung können Zweideutigkeiten in der Interpretation ausgeschlossen und formale Beweistechniken angewendet werden. Bisherige formale Verifikationen von Sicherheitspolitiken beinhalten im allgemeinen den Nachweis von Safety-Eigenschaften. Wir verlangen zusätzlich die Betrachtung von Security-Eigenschaften, wobei aus heutiger Sicht beide Arten von Eigenschaften stets getrennt in unterschiedlichen Formalismen verifiziert werden. Die Arbeit stellt eine gemeinsame Spezifikations- und Verifikationsmethodik mit Hilfe von Observer-Modellen vor, die sowohl den Nachweis von Safety-Eigenschaften in einem TLA-Modell als auch den Nachweis von Security-Eigenschaften kryptografischer Protokolle in einem induktiven Modell erlaubt. Da wir alle Spezifikationen und Verifikationen im Werkzeug VSE-II durchführen, bietet das formale Modell der Sicherheitspolitik nicht nur einen abstrakten Blick auf das System, sondern dient gleichzeitig als abstrakte Systemspezifikation, die es in weiteren Entwicklungsschritten in VSE-II zu verfeinern gilt. Die vorgestellte Methodik der Integration beider Systemmodelle in VSE-II führt somit zu einer erhöhten und nachweisbaren Qualität von Sicherheitspolitiken und von Sicherheitssystemen. / Security systems that use smart cards are nowadays an important part of our daily life, which becomes increasingly dependent on the reliability of such systems, for example cash cards, electronic health cards or identification documents. Since a security policy states both the main security objectives and the security functions of a certain security system, it is the basis for the reliable system development. This work focuses on multi-applicative smart card operating systems and addresses new security objectives regarding the applications running on the card. As the quality of the operating system is determined by the underlying security policy, its correctness is of crucial importance. A formalization of it first provides an unambiguous interpretation and second allows for the analysis with mathematical precision. The formal verification of a security policy generally requires the verification of so-called safety properties; but in the proposed security policy we are additionally confronting security properties. At present, safety and security properties of formal system models are verified separately using different formalisms. In this work we first formalize a security policy in a TLA system specification to analyze safety properties and then separately verify security properties using an inductive model of cryptographic protocols. We provide a framework for combining both models with the help of an observer methodology. Since all specifications and proofs are performed with the tool VSE-II, the verified formal model of the security policy is not just an abstract view on the security system but becomes its high level specification, which shall be refined in further development steps also to be performed with the tool. Hence, the integration of the two approaches within the tool VSE-II leads to a new quality level of security policies and ultimately of the development of security systems.