Dokument: Rapid Creation of Interactive Formal Prototypes for Validating Safety-Critical Systems

Titel:	Rapid Creation of Interactive Formal Prototypes for Validating Safety-Critical Systems
URL für Lesezeichen:	https://docserv.uni-duesseldorf.de/servlets/DocumentServlet?id=42485
URN (NBN):	urn:nbn:de:hbz:061-20170530-104959-8
Kollektion:	Dissertationen
Sprache:	Englisch
Dokumententyp:	Wissenschaftliche Abschlussarbeiten » Dissertation
Medientyp:	Text
Autor:	Ladenberger, Lukas [Autor]
Dateien:	[Dateien anzeigen] Adobe PDF [Details] 6,82 MB in einer Datei [ZIP-Datei erzeugen] Dateien vom 30.05.2017 / geändert 30.05.2017
Beitragende:	Prof. Dr. Leuschel, Michael [Gutachter] Prof. Dr. Gorm Larsen, Peter [Gutachter]
Dewey Dezimal-Klassifikation:	000 Informatik, Informationswissenschaft, allgemeine Werke » 004 Datenverarbeitung; Informatik
Beschreibungen:	The application of formal methods to the development of interactive safety-critical systems usually involves a multidisciplinary team with different roles and expertise (e.g. formal engineers, user interface designers and domain experts). For instance, it is important for the formal engineer to get feedback from the domain expert and the user interface engineer to further develop the formal specification. On the other hand, the domain expert needs to check whether his expectations of the application domain are met in the formal specification and the user interface engineer needs to prevent conflicts between the system’s functionality and the user interface design. In general, these tasks deal with the question “Are we building the right system?” and are typically performed with of validation techniques. Animation is a popular validation technique for state-based formal methods such as classical-B and Event-B. The purpose of animation is to inspect the desired behavior of a formal specification by executing it. It can also be used to walk-through and analyse scenarios within a multidisciplinary team. However, a formal specification typically becomes complex and large which can make the analysis of a specific aspect of the system using animation difficult and error prone even for formal engineers. Furthermore, while formal engineers have the necessary expertise (e.g. the mathematical notation often used in formal methods) for performing animation techniques, other roles such as user interface engineers or domain experts may not be well versed in formal methods. Consequently, animation techniques may become inaccessible to non-formal method experts. In this thesis, we present a novel graphical environment called BMotionWeb that provides features for the lightweight validation of interactive safety-critical systems by creating interactive formal prototypes. An interactive formal prototype complements the use of animation with interactive data visualization, a technique to support human understanding by viewing and interacting with pictures or diagrams rather than by examining a substantial amount of data (e.g. numerical or textural data). As the famous saying states, “one picture is worth ten thousand words”. We present a reference implementation for BMotionWeb based on the ProB animation engine which enables the rapid creation of interactive formal prototypes for the state-based formal methods classical-B and Event-B and present an extension for the event-based formal method CSPM. In order to demonstrate the use of BMotionWeb, we present various case studies, including interactive systems, industrial case studies, and case studies for teaching formal methods. Der Einsatz von formalen Methoden für die Entwicklung von interaktiven sicherheitskritischen Systemen involviert typischerweise verschiedene Rollen und Fachkenntnisse, wie zum Beispiel Formale-Methoden-Ingenieure, Benutzeroberflächen-Entwickler und Domänen-Experten. So ist zum einen der Formale-Methoden-Ingenieur auf Feedback vom Domänen-Experten und dem Benutzeroberflächen-Entwickler angewiesen, anderseits ist es die Aufgabe vom Domänen-Experten zu prüfen, ob die formale Spezifikation die Erwartungen bezüglich der Domäne erfüllt. Weiterhin muss der Benutzeroberflächen-Entwickler verhindern, dass es keine Fehlanpassungen zwischen der Systemfunktionalität und dem Design der Benutzeroberfläche gibt. Im Allgemeinen beschäftigen sich diese Aufgaben mit der Frage “Bauen wir das richtige System?” und werden normalerweise mit Hilfe von Techniken zur Validierung ausgeführt. Eine der bekannten Techniken für die Validierung von zustandsbasierten formalen Methoden wie classical-B und Event-B ist Animation. Der Zweck von Animation ist es eine formale Spezifikation auszuführen, um so die Inspektion vom Systemverhalten zu ermöglichen. Jedoch werden formale Spezifikationen typischerweise komplex und umfangreich, so dass der Einsatz von Animation für die Analyse von sicherheitskritischen Systemen schwer und fehleranfällig werden kann - sogar für Formale-Methoden-Ingenieure. Zudem haben Domänen-Experten oder Benutzeroberflächen-Entwickler meist unzureichende Kenntnisse im Einsatz von formalen Methoden (zum Beispiel über die mathematische Notation, welche bei formalen Methoden oft eingesetzt wird), was dazu führen kann, dass Animation nicht verwendet werden kann. In dieser Arbeit präsentieren wir BMotionWeb, ein neues grafisches Tool, das ermöglicht interaktive formale Prototypen für die leichtgewichtige Validierung von interaktiven sicherheitskritischen Systemen zu erstellen. Ein interaktiver formaler Prototyp kombiniert Animation mit interaktiver Datenvisualisierung, einer Technik, die benutzt wird, um Menschen bei der Analyse von Daten (z.B. numerische or textuelle Daten) zu unterstützen. Dabei folgt interaktive Datenvisualisierung ganz dem Motto “Ein Bild sagt mehr als tausend Worte” und repräsentiert die Daten als Bilder oder Diagramme, welche dann als Grundlage für die Analyse dienen. Wir präsentieren eine Referenzimplementierung von BMotionWeb basierend auf dem ProB Animator, welche das Erstellen von interaktiven formalen Prototypen für die zustandsbasierten formalen Methoden classical-B und Event-B und der eventbasierten formalen Methode CSPM ermöglicht. Um den Nutzen von BMotionWeb zu demonstrieren, präsentieren wir verschiedene Fallbeispiele einschließlich interaktive Systeme, industrielle Fallbeispiele und Fallbeispiele für das Unterrichten von formalen Methoden.
Lizenz:	Urheberrechtsschutz
Fachbereich / Einrichtung:	Mathematisch- Naturwissenschaftliche Fakultät » WE Informatik » Softwaretechnik und Programmiersprachen
Dokument erstellt am:	30.05.2017
Dateien geändert am:	30.05.2017
Promotionsantrag am:	14.11.2016
Datum der Promotion:	07.02.2017