Dokument: Constraint Modelling and Data Validation Using Formal Specification Languages

Titel:	Constraint Modelling and Data Validation Using Formal Specification Languages
URL für Lesezeichen:	https://docserv.uni-duesseldorf.de/servlets/DocumentServlet?id=44230
URN (NBN):	urn:nbn:de:hbz:061-20171218-100210-6
Kollektion:	Dissertationen
Sprache:	Englisch
Dokumententyp:	Wissenschaftliche Abschlussarbeiten » Dissertation
Medientyp:	Text
Autor:	Schneider, David [Autor]
Dateien:	[Dateien anzeigen] Adobe PDF [Details] 4,21 MB in einer Datei [ZIP-Datei erzeugen] Dateien vom 01.12.2017 / geändert 01.12.2017
Beitragende:	Prof. Dr. Leuschel, Michael [Betreuer/Doktorvater] Prof. Dr. Ledru, Yves [Gutachter]
Dewey Dezimal-Klassifikation:	000 Informatik, Informationswissenschaft, allgemeine Werke » 004 Datenverarbeitung; Informatik
Beschreibungen:	Formal methods provide rich and expressive specification languages to reason about and to describe systems at a high abstraction level. These methods are usually supported by powerful tools to verify the correctness of the specifications by different means such as proof or model checking. But is it possible to express non-trivial constraint satisfaction problems in these specification languages and to use such a formal model at runtime for problem solving and data validation? Are languages and the tools powerful enough to enable this usage scenario? These are the central questions we explore in this thesis. We look at these questions with a particular focus on the B Method – a state based formal method for software development – and the ProB tool – an animator and model checker for the B Method. We begin by studying the use of the B language, a part of the B method, not only as a specifications language but also as a modelling language for a wide range of challenging constraint based problems. We show on several puzzles and case studies that it is possible to formalize these problems elegantly using B. We also show that for many problems it is possible to solve these formalizations using ProB. We use our results on a larger case study about performing data validation of university curricula using a formal specification. In this case study we use the B language to model and validate the feasibility of university curricula from a students’ perspective and show that ProB can efficiently solve this validation problem. In particular, we show that it is possible to embed ProB in an application and solve this validation problem at runtime using our B model. Afterwards, we will present a general structure of a data validation project in B and outline common challenges along with various solutions. This discussion is rooted in the results and experiences gathered on our case study and on a second independent one. We also discuss possible evolutions of the B language to make it (even) more suitable for such projects. In the course of this thesis we discuss several alternative modelling approaches and how they relate to B and ProB. To conclude, we perform an in-depth evaluation where we compare our B and ProB based approach to several other tools and languages that can be used for this kind of validation task. We conclude that our approach of using B not only as a formal specification language but also as a constraint modelling language can be applied successfully in this scenario. Nevertheless, there are areas where this approach could be improved or extended to better suit this kind of application. We also conclude that ProB produces very good results for the high abstraction level of the language, that it is in many cases faster than brute force solutions and that it is comparable to dedicated constraint solving approaches. Formale Methoden bieten ausdrucksstarke Spezifikationssprachen um Probleme systematisch zu analysieren und diese mit einem hohen Abstraktionsgrad zu beschreiben. Mit einer Spezifikation werden Eigenschaften eines Systems beschrieben. Um deren Korrektheit zu überprüfen sind Softwarewerkzeuge zentral. Diese erlauben es durch unterschiedliche Techniken, wie Beweise oder Model-Checking, solche Spezifikationen zu verifizieren. Ist es darüber hinaus möglich nicht-triviale Constraint-Satisfaction Probleme in diesen Spezifikationssprachen auszudrücken und ein solches Model zur Laufzeit zu verwenden um Probleme zu lösen und Datenvalidierung durchzuführen? Sind die existierenden Sprachen und Werkzeuge ausdrucksstark und mächtig genug für diesen Einsatzzweck? Dies sind die zentralen Fragen, die in dieser Arbeit erörtert werden. Sie werden mit einem besonderem Augenmerk auf die B-Methode – eine zustandsbasierte formale Methode zur Softwareentwicklung – und dem ProB Werkzeug – ein Animator und Model-Checker für die B-Methode – untersucht. Zunächst wird die Verwendung der B-Sprache, ein Teil der B-Methode, nicht nur als Spezifikationssprache sondern auch als Sprache um Constraints zu beschreiben diskutiert. Anhand einer Reihe unterschiedlicher Puzzles und Fallstudien wird gezeigt, dass es möglich ist, diese mit der B-Sprache auf elegante Art und Weise zu formalisieren und dass es möglich ist, diese Problembeschreibungen mit Hilfe vom ProB auszuwerten. Diese Ergebnisse bilden die Grundlage einer umfangreichen Fallstudie über die Validierung von Hochschulstudienplänen mit Hilfe einer formalen B-Spezifikation. Insbesondere wird gezeigt, dass es möglich ist ProB in eine Anwendung einzubetten um dieses Validierungsproblem zur Laufzeit zu lösen. Aufbauend auf den Ergebnissen und Erfahrungen, die bei der zuvor erwähnten Fallstudie und bei einer zweiten unabhängigen Fallstudie gesammelt wurden, wird eine allgemeine Struktur für B-basierte Datenvalidierungsprojekte vorgestellt. Außerdem wer- den Probleme, die bei diesen Projekten auftreten können, sowie mögliche Lösungsansätze diskutiert. Im Verlauf dieser Arbeit werden verschiedene alternative Modellierungsansätze diskutiert, sowie mit B und ProB verglichen. Den Abschluss dieser Arbeit bildet ein systematischer Vergleich dieses auf B und ProB basierenden Ansatzes zu alternativen Methoden, die für die untersuchten Validierungsprobleme eingesetzt werden können. Aus diesem Vergleich lässt sich schließen, dass B nicht nur als formale Spezifikationssprache sondern in diesem Kontext auch als Costraint-Modellierungssprache eingesetzt werden kann. Eines der Ergebnisse dieser Arbeit ist, dass ProB sehr gute Ergebnisse bei der untersuchten Art von Validierungsproblemen, insbesondere unter Berücksichtigung des Abstraktionsgrades der Sprache, liefert. Ferner ist ProB in vielen Fällen schneller als Brute-Force-Lösungen und liefert Ergebnisse, die mit dedizierten Constraint-Solving-Ansätzen vergleichbar sind.
Lizenz:	Urheberrechtsschutz
Fachbereich / Einrichtung:	Mathematisch- Naturwissenschaftliche Fakultät » WE Informatik » Softwaretechnik und Programmiersprachen
Dokument erstellt am:	18.12.2017
Dateien geändert am:	18.12.2017
Promotionsantrag am:	10.05.2017
Datum der Promotion:	12.07.2017