Dokument: Supporting Validation and Verification of State-Based Formal Models

Titel:Supporting Validation and Verification of State-Based Formal Models
URL für Lesezeichen:https://docserv.uni-duesseldorf.de/servlets/DocumentServlet?id=36786
URN (NBN):urn:nbn:de:hbz:061-20160404-143308-5
Kollektion:Dissertationen
Sprache:Englisch
Dokumententyp:Wissenschaftliche Abschlussarbeiten » Dissertation
Medientyp:Text
Autor: Plagge, Daniel [Autor]
Dateien:
[Dateien anzeigen]Adobe PDF
[Details]2,33 MB in einer Datei
[ZIP-Datei erzeugen]
Dateien vom 04.04.2016 / geändert 04.04.2016
Beitragende:Prof. Dr. Leuschel, Michael [Gutachter]
Prof. Dr. Denecker, Marc [Gutachter]
Stichwörter:Validation, Verification, Formal Methods, Formal Models, Model Checking, B-Method, Z Notation
Dewey Dezimal-Klassifikation:000 Informatik, Informationswissenschaft, allgemeine Werke » 004 Datenverarbeitung; Informatik
Beschreibungen:The four presented articles in this work address distinct aspects of supporting the development, validation and verification of state-based systems with formal models. State-based models describe a system by defining what constitutes a state and when and how a transition to a new state can be performed.
Software tools play a central role in supporting system development. ProB is such a tool that visualises and analyses the behaviour of a formal specified system via “animation” and that performs automated model checking to discover errors in the specification. Animation and model checking contribute to the development of critical software systems and the validation of systems under development.
Each of the presented researches had lead to an implementation of an extension to the development and validation tool ProB that has been written originally for the B method.
The first presented article explains how ProB has been extended to support the widely-used specification language Z. It shows how errors were found just by animating specifications written in Z.
Another extension to ProB covers also a specification language, Event-B, a successor of the B method. A main characteristic of Event-B is its refinement mechanism and the main challenge was to support refinement and allow a user to identify problems in refined models.
With formulas in temporal logic it is possible to express requirements with dependencies between a sequence of states. The extension presented in the third part verifies whether a model fulfils the given properties and therefore it allows to validate if the model meets the requirements.
The last presented article applies a SAT solver via an external library to specifications loaded into ProB. SAT solving is used as a complementary technique in ProB to improve its capability to animate specifications. A specific aspect of this translation is that the target formalism is less expressive than the formalism supported by ProB and not all encountered parts of a problem statement can be translated effectively.
For every presented article it is shown how it contributes to validation and verification of systems and which of ProB’s components are affected by the implementation of the corresponding extension.

Zustandsbasierte Modelle beschreiben ein System, in dem definiert wird, was einen Zustand des Systems ausmacht und auf welche Weise und unter welchen Umständen Zustandswechsel vollzogen werden können. Die hier vorgestellte Arbeit befasst sich mit der Unterstützung von Entwicklung, Validierung und Verifikation von Systemen, die mittels zustandsbasierten formalen Modellen entworfen werden.
Eine zentrale Rolle bei der Unterstützung der Systementwicklung bilden Softwarewerkzeuge. Bei ProB handelt es sich um solch ein Werkzeug, welches das Verhalten formaler Spezifikationen für einen Benutzer begreifbar macht („Animation“) und automatisierte Modellprüfungen darauf ausführt. Dies trägt bei der Entwicklung kritischer Software mit zur Validierung und Verifizierung des zu entwickelnden Systems bei. Alle Arbeiten resultierten in konkrete Erweiterungen des Entwicklungs- und Validierungswerkzeuges ProB, das ursprünglich für die B-Methode geschrieben wurde.
Zunächst wird erläutert wie ProB erweitert wurde, um die Spezifikationssprache Z zu unterstützen. Es wird gezeigt, wie allein durch Animation von Z Spezifikationen sicherheitskritischer Anwendungen in diesen Fehler gefunden werden konnten.
Auch die nächste Arbeit erweitert ProB um eine Spezifikationssprache. Ein wesentliches Merkmal von Event-B ist die Möglichkeit zur Modellverfeinerung („Refinement“), auf deren Unterstützung ein besonderes Augenmerk gelegt wurde. Entwickler sollen in die Lage versetzt werden, schnell Probleme im Refinement zu entdecken und zu beheben.
Mittels temporal-logischer Formeln lassen sich Anforderungen an das System formulieren, die sich über eine Abfolge von Zuständen und Zustandsänderungen erstrecken. Die vorgestellte Erweiterung für ProB kann prüfen, ob ein System diese Anforderungen erfüllt.
Der letzte Teil befasst sich damit, wie Modelle, die von ProB analysiert werden, so übersetzt werden könne, dass mit Hilfe von SAT Solvern Lösungen gesucht werden können. SAT Solving steht damit als komplementäre Technologie zur Verfügung, um um die Möglichkeiten zur Analyse komplexer Modelle zur verbessern.
Zu allen Arbeiten wird kurz vorgestellt, wie sie zur Validierung und Verifikation von Systemen beitragen und welche Komponenten von ProB die Implementierung der entsprechenden Erweiterung betrifft.
Lizenz:In Copyright
Urheberrechtsschutz
Fachbereich / Einrichtung:Mathematisch- Naturwissenschaftliche Fakultät » WE Informatik » Softwaretechnik und Programmiersprachen
Dokument erstellt am:04.04.2016
Dateien geändert am:04.04.2016
Promotionsantrag am:15.09.2015
Datum der Promotion:19.11.2015
english
Benutzer
Status: Gast
Aktionen