Verifikation von Statecharts durch struktur- und eigenschaftserhaltende Datenabstraktion
Helke, Steffen
In dieser Arbeit wird ein Ansatz zur Verifikation von Statecharts mit unendlichen Daten vorgestellt. Es wird ein Verfahren konzipiert, mit dem die Gültigkeit einer temporallogischen Formel des universalen Fragements der CTL für eine Statecharts-Spezifikation überprüft werden kann. Das entwickelte Verfahren beruht auf einer struktur- und eigenschaftserhaltenden Datenabstraktionstechnik und ist in einem logikbasierten Framework prototypisch umgesetzt. Eine notwendige Voraussetzung zur Umsetzung des Vorhabens ist der Aufbau einer Beweisinfrastruktur in dem interaktiven Theorembeweiser Isabelle/HOL, in der eine Datenabstraktion für Statecharts-Spezifikationen maschinengestützt vorgenommen werden kann. Zunächst wird in Isabelle/HOL die abstrakte Syntax und eine synchrone Schrittsemantik der Spezifikationssprache Statecharts formalisiert. Grundlage der Formalisierung sind Hierarchische Automaten, die eine strukturelle Zerlegung von Statecharts in Sequentielle Automaten erlauben. Die aus der Literatur bekannte Beschreibung Hierarchischer Automaten wird durch zwei Optimierungen für die Zwecke eines Theorembeweisers adaptiert. Zum einen werden in der Formalisierung Konstruktionsoperatoren eingeführt, mit denen Hierarchische Automaten schrittweise aus ihren sie definierenden Sequentiellen Automaten zusammengesetzt werden können. Zum anderen wird die baumartige Struktur Hierarchischer Automaten durch einen primitiv-rekursiven Datentyp repräsentiert und darauf aufbauend die Syntax und Semantik von Statecharts durch rekursive Konstantendefinitionen beschrieben. Durch dieses Vorgehen ist es möglich, in der Beweisführung auf effiziente Induktionstaktiken zurückzugreifen. Ein wichtiger Beitrag der Arbeit besteht in der Formalisierung komplexer Datenräume für Statecharts. Hierfür werden partitionierte Datenräume, vollständige und partielle Datenraumbelegungen, sowie totale und partielle Update-Funktionen eingeführt. Mit Hilfe der Definitionen wird das komplizierte Verhalten auf den Datenräumen formuliert. Teil der Beschreibung ist eine Interleaving-Semantik, mit der die Effekte beim konkurrierenden Schreiben synchron ausgeführter Update-Funktionen angegeben wird. Neben der Beschreibung von Statecharts mit Datenräumen wird in der Arbeit eine Formalisierung der temporalen Logik CTL angegeben, deren Semantik auf Kripkestrukturen basiert. Es wird ein Operator definiert, mit dem aus einem Hierarchischen Automaten eine sein Verhalten definierende Kripkestruktur abgeleitet werden kann. Mit Hilfe des Operators kann ausgedrückt werden, dass eine CTL-Formel in einer Statecharts-Spezifikation erfüllt ist. Der Hauptbeitrag der Arbeit besteht in der Konzeption einer Abstraktionstheorie, mit der der Datenraum eines Hierarchischer Automaten für eine gegebene Abstraktionsfunktion abstrahiert werden kann. Die Technik basiert auf der Konstruktion von Überapproximationen und ist für das universale Fragment der CTL eigenschaftserhaltend. Das Ergebnis der Abstraktion ist durch einen Hierarchischen Automaten repräsentiert. Das Verfahren ist strukturerhaltend, d.h. die strukturellen Merkmale eines zu abstrahierenden Hierarchischen Automaten bleiben während der Abstraktion erhalten. Die Abstraktion erfolgt in kompositionaler Art und Weise. Zunächst wird ein zu abstrahierender Hierarchischer Automat in die ihn definierenden Sequentiellen Automaten zerlegt und diese separat voneinander abstrahiert. Anschließend werden die abstrahierten Einzelteile zu einem Hierarchischen Automaten zusammengefügt. Um den praktischen Umgang mit dem Framework zu erleichtern, werden abschließend zwei Taktiken vorgestellt, die im Rahmen der Arbeit konzipiert und in dem Theorembeweiser Isabelle/HOL implementiert worden sind. Die Taktiken nutzen neben Isabelle auch andere Verifikationswerkzeuge, um den Beweisprozess effizienter zu gestalten. Die Tragfähigkeit des Ansatzes wird für eine Fallstudie gezeigt.
In this thesis we present an approach for verifying Statecharts including infinite data spaces. We conceive a technique for checking that a formula of the universal fragment of the temporal logic CTL is satisfied by a specification written as a Statechart. The developed approach is based on a property-preserving abstraction technique that additionally preserves structure. It is prototypically implemented in a logic-based framework. As a first important step to realize this project we build a proof infra-structure for Statecharts in the interactive theorem prover Isabelle/HOL, which constitutes a basis for defining a mechanized data abstraction process. First, we formalize in Isabelle/HOL the abtract syntax and a synchronous step semantics for the specification language Statecharts. The formalization is based on Hierarchical Automata which allow a structural decomposition of Statecharts into Sequential Automata. We adapt the description of Hierarchical Automata as known in the literature in two ways optimizing them for theorem provers. First, we introduce calculating operators in order to construct a Hierarchical Automaton in a stepwise manner from its defining Sequential Automata. Second, we represent the tree-like structure of Hierarchical Automata by a primitive recursive data type. Based on this type we describe the syntax and semantics of Statecharts by recursive constant definitions. This procedure allows to improve proofs by efficient inductive tactics. An important contribution of this thesis is the formalization of complex data spaces, which can be included in a Statechart. Therefore, we introduce partitioned data spaces, complete and partial data assignments, as well as total and partial update functions. Using these definitions we formalize the complicated behaviour on the data spaces. This formalization includes an interleaving semantics in order to describe the effects of synchronous executed update functions, that write into a data space concurrently. In addition to the formalization of Statecharts including data spaces we give a formal description of the temporal logic CTL whose semantics is based on Kripke Structures. We define an operator constructing, for a given Hierarchical Automaton, its defining behaviour by a Kripke Structure. Using this operator we can express that a CTL formula must be satisfied by a Statchart. The main contribution of this thesis is a data abstraction theory, which can be used to abstract the data space of a Hierarchical Automaton for a given abstraction function. The technique is based on constructing over-approximations and is property-preserving for the universal fragment of the CTL. The result of an abstraction is represented by a Hierarchical Automaton. The technique is structure-preserving, which means that the structural properties of a Hierarchical Automaton is preserved in an abstraction process. The abstraction is designed in a compositional way. First, we decompose a Hierarchical Automaton into its defining Sequential Automata. Second, we abstract each Sequential Automaton independently. Finally, we compose the abstracted parts into a Hierarchical Automaton. For reasons of practicability, we finally present two tactics. The scope of this thesis includes a design and an implementation of these tactics in the theorem prover Isabelle/HOL. In order to make the proofs more efficient, these tactics are additionally supported by other verification tools. The practicability of the presented approach is shown by a case study.
