[Back]


Doctor's Theses (authored and supervised):

S. Gabmeyer:
"New Model Checking Techniques for Software Systems Modeled with Graphs and Graph Transformations";
Supervisor, Reviewer: G. Kappel, M. Seidl; Institut für Softwaretechnik und Interaktive Systeme, 2015; oral examination: 2015-08-10.



English abstract:
In today's software, no matter how security and safety critical it may be, defects and failures
are common. With the rising complexity of software and our growing dependency
on its correct functioning as it permeates our every day life the software development
process requires new approaches to integrate formal veri cation techniques. This thesis
presents approaches on e ciently verifying software systems described by model-driven
software development artifacts. These artifacts comprise the implementation of the
system and consist of both structural and behavioral models. We present two model
checking approaches, MocOCL and Gryphon, to verify the temporal speci cation of a
system against its model-based implementation. Central to our approach is the twofold
use of graphs to describe the system under veri cation. First, we describe the admissible
static structure of an instance of the system by means of attributed type graphs
with inheritance and containment relations, often referred to as metamodel. Second, we
represent a state of the system as an object graph that enumerates a system's active
objects, the references among them, and their attribute values. A change in the system,
e.g., the deletion of an object or the modi cation of an attribute value, triggers
a state change. The behavior of the system is thus described by actions that modify
the state of the system. In this thesis we employ graph transformations to model such
state-changing actions as they provide suitable means to formally describe modi cations
on graphs. The speci cation of the system, on the other hand, is written in our temporal
extension of the Object Constraint Language (OCL) that is based on Computation Tree
Logic (CTL). A speci cation written in our CTL extension for OCL, called cOCL, can
be veri ed against a model-based implementation of the system with our explicit-state
model checker MocOCL. Gryphon aims to increase the e ciency and scalability of the
veri cation process and implements a symbolic model checking approach, that focuses
the veri cation on safety speci cations.
The work presented in this thesis also encompasses a survey and a feature-based classi
cation of veri cation approaches that can be used to verify artifacts of model-driven
software development. Methodologically, it provides the motivation for our work on Mo-
cOCL and Gryphon. Both our approaches are novel in their own respect; MocOCL
for its capability to verify CTL-extended OCL expressions and Gryphon for its use of
relational logic to build a symbolic representation of the system that can be veri ed with
any model checker participating in the Hardware Model Checking Competition. Finally,
MocOCL and Gryphon are evaluated performance-wise on a set of three representative benchmarks that demonstrate the model checkers' preferred elds of application and its
limitations.

German abstract:
Die steigende Komplexit at von Software und der gleichzeitig wachsenden Abh angigkeit
unserer Gesellschaft von ihrer korrekten Funktionsweise erfordert die Integration von
formalen Methoden in den Softwareentwicklungsprozess. In dieser Disseration werden
daher Ans atze und Techniken vorgestellt um Softwareartefakte zu veri zieren, die im
Zuge eines modellgetriebenen Entwicklungsprozess erstellt werden. Im Konkreten untersucht
die Arbeit Ans atze zur Veri kation von Struktur- und Verhaltensmodellen. Damit
einhergehend werden zwei Model Checker, n amlich MocOCL und Gryphon|vorgestellt,
die die modellbasierte Implementierung eines System gegen deren temporale
Spezi kation veri zieren. Graphen nehmen in diesen beiden Ans atzen eine zentrale Rolle
ein, da sie sowohl zur Beschreibung der Struktur des Systems als auch zur Beschreibung
des Verhaltens des Systems verwendet werden. W ahrend mit Hilfe von attributierten
Typgraphen, oft auch als Metamodelle bezeichnet, welche Vererbungs- und Kompositionsbeziehungen
enthalten, die zul assige Struktur des Systems erfasst wird, dienen Objektgraphen
zur Beschreibung des Zustandes des System und listen zu diesem Zweck alle
aktiven Objekte, die Beziehungen zwischen diesen und deren aktuelle Attributwerte auf.
Eine Ver anderung des Systems, welche beispielsweise durch das L oschen eines aktiven
Objekts oder die Modi kation eines Attributs hervorgerufen wird, hat einen Zustandswechsel
zur Folge, der sich in der Struktur des Objektgraphens widerspiegelt. In dieser
Dissertation wird das Verhalten eines Systems mit Graphtransformationen modelliert,
die es erm oglichen Modi kationen an Graphen formal zu beschreiben. F ur die Spezi kation
des Systems wurde cOCL im Rahmen dieser Dissertation entwickelt. Dabei handelt
es sich um eine temporale Erweiterung der Object Constraint Language (OCL), die
Operatoren der Computation Tree Logic (CTL) in OCL integriert. In weitere Folge kann
nun die Richtigkeit eines Systems, dessen Struktur mit Hilfe von attributierten, getypten
Graphen mit Vererbungs- und Kompisitionseziehungen beschrieben wird und dessen
Verhalten mit Graphtransformationen modelliert wird, in Hinblick auf seine in cOCL
formulierte Spezi kation mit dem Model Checker MocOCL veri ziert werden. Mit
Gryphon wurde ein auf Performance und Skalierbarkeit ausgerichteter Model Checker
entworfen, mit dem Safety-Spezi kationen e zient veri ziert werden k onnen.
Zus atzlich werden in dieser Dissertation eine Studie und eine merkmalbasierte Klassi
kation von Veri kationsans atzen vorgestellt, die die Veri kation von modellbasierte
Softwareimplementierungen erm oglichen. Diese Studie und die daraus resultierende Klassi
kation bildeten aus methodischer Sicht die Motivation f ur die Arbeiten an MocOCL
und Gryphon, die in dieser Hinsicht beide einen neuartigen Ansatz beisteuern. Au erdem beinhaltet die Arbeit eine umfassende Performance-Evaluierung von MocOCL und
Gryphon, die anhand von drei repr asentativen Benchmarks St arken und Einschr ankungen
der Model Checker aufzeigt.

Keywords:
MocOCL, CTL, Gryphon

Created from the Publication Database of the Vienna University of Technology.