Symbolic Methods for the Verification of Software Models

Symbolic Methods for the
Veriﬁcation of Software Models
DISSERTATION
submitted in partial fulﬁllment of the requirements for the degree of
Doktor/in der technischen Wissenschaften
by
Magdalena Widl
Registration Number 0327059
to the Faculty of Informatics
at the Vienna University of Technology
Advisor: Ao. Univ.-Prof. Dr. Uwe Egly
Advisor: Assist.-Prof. Dr. Martina Seidl
The dissertation has been reviewed by
(Ao. Univ.-Prof. Dr. Uwe Egly)
(Prof. Dr. Hans Kleine Büning)
Wien, November 18, 2015
(Magdalena Widl)
Technische Universität Wien
A-1040 Wien � Karlsplatz 13 � Tel. +43-1-58801-0 � www.tuwien.ac.at
Abstract
One of the major challenges in modern software engineering is dealing with the increasing complexity of software systems. The new paradigm of model-driven engineering (MDE) promises to
handle this complexity using the abstraction power of software models based on languages such
as the Uniﬁed Modeling Language (UML). The objective of MDE is to generate executable code
from a set of diagrams with little or no intervention of a developer. These diagrams are referred
to as model of the system to be implemented. Usually multi-view models are employed, where
each diagram shows a different view on the system, altogether providing a holistic representation. This shift from code-centric development to MDE requires a modeling language based on
a solid formal semantics, which is considered one of the major current challenges in MDE research and in future improvements of the UML. Further, with this high valorization of software
models, also stronger requirements on their consistency come along since errors introduced on
the model level can result in faulty code. The models are central to the evolution of a software
system and therefore undergo continuous and often parallel modiﬁcations that can introduce inconsistencies. However, necessary consistency management tasks are often too cumbersome to
be performed manually due to the size of the models. Hence, automated methods are required.
In this work we formalize a modeling language based on the UML. Our language contains
two views: the state machine diagram and the sequence diagram. We then identify three problems that can occur in models based on this language. The Sequence Diagram Merging Problem
deals with merging two modiﬁed versions of a sequence diagram in a way that keeps them
consistent with the set of state machines they are related to. The State Machine Reachability
Problem asks whether a combination of states in a set of state machines can be reached from
some global state by sending and receiving messages between the state machines. The Sequence
Diagram Model Checking Problem asks whether a sequence diagram is consistent with the set
of state machines it instantiates. For each problem, we propose an encoding to the satisﬁability
problem of propositional logic (SAT) in order to solve it with an off-the-shelf SAT solver and
we determine its computational complexity. We evaluate our approaches based on a set of handcrafted models and on grammar-based whitebox fuzzing, for which we develop a random model
generator. The results of our experiments show that we can solve instances of these problems of
reasonable size on standard hardware with state-of-the-art SAT solvers.
v
Kurzfassung
Der Umgang mit der zunehmenden Komplexität moderner Softwaresysteme stellt eine der größten Herausforderungen der modernen Softwareentwicklung dar. Modellgetriebene Entwicklung
(engl. model-driven engineering, MDE) verspricht einen einfacheren Umgang mit dieser Komplexität durch Nutzung der Abstraktionsfähigkeiten modellbasierter Sprachen wie zum Beispiel
der Uniﬁed Modeling Language (UML). Das Ziel von MDE ist es von einer Menge an Diagrammen, dem Modell für das zu entwickelnde System, lauffähigen Programmcode ohne oder
mit minimaler Zuhilfenahme eines Entwicklers automatisch zu generieren. Für diesen Zweck
werden meist Modelle mit mehrfachen Sichten verwendet. Solche Modelle enthalten mehrere
Arten von Diagrammen, wobei jede Art eine andere Sicht auf das System ermöglicht und die
Kombination der Diagramme das System in seiner Gesamtheit beschreibt.
Dieser Wechsel des Fokus von textuellem Programmiercode auf die Softwaremodelle der
MDE verlangt nach einer über eine solide formale Semantik verfügenden Modellierungssprache.
Die Entwicklung einer solchen Modellierungssprache gilt als eine der größten Herausforderungen in der Forschung zu MDE und für zukünftige Verbesserungen der UML. Weiters bringt diese
wesentliche Aufwertung der Softwaremodelle strengere Anforderungen bezüglich deren Konsistenz mit sich, da Fehler auf Modellebene sich in den Programmcode weiterpropagieren. Ihre
neue Führungsrolle im Entwicklungsprozess stellt die Modelle ausserdem in den Mittelpunkt
der Sofwareevolution, wodurch sie häuﬁgen und oftmals parallelen Änderungen ausgesetzt sind.
Die damit entstehenden Aufgaben im Bereich des Konsistenzmanagements, des Testens und der
Fehlerbehebung sind bedingt durch die Größe der Modelle zu komplex um manuell durchgeführt
zu werden. Automatische Methoden sind daher unumgänglich.
In dieser Arbeit formalisieren wir eine Modellierungssprache, die auf der UML basiert und
zwei Sichten beinhaltet, nämlich das Zustandsdiagramm und das Sequenzdiagramm. Wir identiﬁzieren drei Probleme, die in auf dieser Sprache basierenden Modellen auftreten können. Das
Sequence Diagram Merging Problem befasst sich mit der Integration von parallel an einem
Sequenzdiagramm durchgeführten Änderungen mit dem Ziel, ein mit einer Menge von Zustandsdiagrammen konsistentes Sequenzdiagramm zu erstellen. Das State Machine Reachability
Problem beschreibt, ob eine Kombination aus in verschiedenen Zustandsdiagrammen enthaltenen Zuständen von einem gegebenen globalen Zustand erreichbar ist. Das Sequence Diagram
vii
Model Checking Problem fragt, ob ein Sequenzdiagramm konsistent ist mit der Menge an Zustandsdiagrammen, die es instanziiert. Für jedes der drei Probleme erstellen wir eine Kodierung
als aussagenlogisches Erfüllbarkeitsproblem, das mit einem gängigen, frei verfügbaren Solver
gelöst werden kann, und ermitteln seine computationale Komplexität. Wir evaluieren unseren
Lösungsansatz mit handgefertigten Instanzen und mittels einer grammatikbasierenden WhiteBox-Fuzzing-Methode, wofür wir einen randomisierenden Modellgenerator entwickeln. Die
Resultate unserer Experimente zeigen, dass Instanzen unserer Probleme von brauchbarer Größe
von einem gängigen Solver auf gängiger Hardware in vertretbarer Zeit gelöst werden können.

Download Report