[Back]

R. Bill:
"Towards Software Model Checking in the Context of Model-Driven Engineering";
Supervisor: G. Kappel, P. Kaufmann, S. Gabmeyer; E188 Institut für Softwaretechnik und Interaktive Systeme, 2014; final examination: 04-10-2014.

The aim of this master thesis is to reduce the conceptual gap between software modeling and model checking. While model checking is successfully applied for hardware verification, it is not widespreadly used in model-driven engineering (MDE). Thus, we tried to reduce this gap by combining modeling and model checking concepts.

This thesis first describes the history and basic idea of both MDE and model checking with a focus on the technologies used in this thesis. Before presenting our new approach, existing solutions are compared. Most approaches propose to extend the Object Constraint Language (OCL) by temporal aspects. This allows to describe the behavior of a software system additionally to various properties of static models. However, one of the main missing features in general seems to be a user-friendly representation of the verification result helpful for debugging. Often, the technical spaces are changed.

With our solution we provide (i) a temporal OCL extension based on the Computational Tree Logic (CTL) and (ii) an OCL extension that introduces path selectors to extract interesting system configurations from the state space. Both OCL extensions were formally defined and implemented. We describe systems in terms of state spaces consisting of EMOF-model states and state transitions containing a mapping between model elements of different states. The system behavior is specified using an initial Ecore model and graph transformations based on the Henshin tool2. The approach, however, is designed to be flexible enough to allow an easy integration of any kind of behavior specification as long as a suitable state space can be derived thereof. Our model checking framework is developed with a focus on delivering not only the results, but also making the system behavior leading to the result comprehensible by providing a suitable tool including a web interface.

The implementation was evaluated in terms of performance to find out the maximum evaluable model size and query complexity. Further, a qualitative user study was conducted for evaluating the CTL extension and the tool. The results of this study indicate that both the CTL-based extension of OCL as well as the tool are a promising first step to integrate model checking in the MDE life cycle.

Das Ziel dieser Diplomarbeit ist, die Welten von Modellprüfung und Softwaremodellierung anzunähern. Während Modellprüfungstechniken inzwischen erfolgreich für die Verifikation von Hardware und Software eingesetzt werden, konnten sie in der modellgetriebenen Softwareentwicklung (MDE) noch nicht Fuß fassen. Eine Ursache dafür könnte sein, dass sich die Begrifflichkeiten in beiden Bereichen noch zu stark unterscheiden. Daher wird in dieser Arbeit versucht, Modellierungs- und Modellprüfungskonzepte zu verbinden. Zunächst werden Geschichte und grundlegende Konzepte von MDE und Modellprüfung mit einem Fokus auf die in dieser Arbeit benutzten Technologien beschrieben. Schließlich werden existierende Ansätze in diesem Bereich verglichen. Die meisten Ansätze schlagen vor, die Object Constraint Language (OCL) um temporale Aspekte zu erweitern. Denn OCL ist zwar gut für die Abfrage von Eigenschaften aus statischen Modellen geeignet, bietet aber kaum Möglichkeiten, ein sich im Zeitverlauf veränderndes Modell zu behandeln. Es gibt aber bislang keine Realisierung dieser Ansätze, bei der die Präsentation der Verifikationsausgabe hilfreich für das Debuggen des Modells ist.

Die in der Diplomarbeit erarbeitete Lösung bietet (i) eine OCL-Erweiterung um zeitliche Aspekte, die auf der Computational Tree Logic (CTL) basiert und (ii) eine OCL-Erweiterung, die Pfadselektoren zur Auswahl interessanter Systemkonfigurationen bereitstellt. Beide OCL-Erweiterungen wurden formal spezifiziert und implementiert. Wir beschreiben Systeme durch Zustandsräume, in denen Zustände aus Ecore-Modellen bestehen. Zustandsübergänge enthalten eine Abbildung zwischen Modellelementen eines Zustands und dessen Nachfolgezustands. Das Systemverhalten wird durch ein Anfangsmodell und Graphtransformationen in Henshin3 beschrieben. Der Ansatz wurde entworfen, flexibel genug für andere Verhaltensspezifikationen zu sein, die einen geeigneten Zustandsraum liefern. Unser Modellprüfungsframework wurde entwickelt, um das Systemverhalten, das zu einem Zustand geführt hat, verständlich zu machen. Dazu wurde ein geeignetes Werkzeug mit einer Webschnittstelle entwickelt.

Die Implementierung wurde hinsichtlich Skalierbarkeit im Bezug auf Eingabemodellgröße und Ausdruckskomplexität überprüft. Ebenso wurde eine qualitative Benutzungsstudie durchgeführt, um die Benutzbarkeit der CTL-Erweiterung und der Webschnittstelle zu überprüfen. Die Ergebnisse zeigen, dass die OCL-Spracherweiterung auf Basis von CTL sowie das entwickelte interaktive Werkzeug einen vielversprechenden Schritt in Richtung Integration von Modellprüfung in den MDE-Lebenszyklus darstellt.

Modellgetriebene Software Entwicklung, Verifikation, Modellprüfung, model-driven engineering, verification, model checking

http://publik.tuwien.ac.at/files/PubDat_227939.pdf