Dokument: On Executing State-Based Specifications and Partial Order Reduction for High-Level Formalisms
| Titel: | On Executing State-Based Specifications and Partial Order Reduction for High-Level Formalisms | |||||||
| URL für Lesezeichen: | https://docserv.uni-duesseldorf.de/servlets/DocumentServlet?id=61784 | |||||||
| URN (NBN): | urn:nbn:de:hbz:061-20230130-080614-7 | |||||||
| Kollektion: | Dissertationen | |||||||
| Sprache: | Englisch | |||||||
| Dokumententyp: | Wissenschaftliche Abschlussarbeiten » Dissertation | |||||||
| Medientyp: | Text | |||||||
| Autor: | Körner, Philipp [Autor] | |||||||
| Dateien: |
| |||||||
| Beitragende: | Prof. Dr. Leuschel, Michael [Betreuer/Doktorvater] Dr. Idani, Akram [Gutachter] | |||||||
| Dewey Dezimal-Klassifikation: | 000 Informatik, Informationswissenschaft, allgemeine Werke » 004 Datenverarbeitung; Informatik | |||||||
| Beschreibung: | This thesis is a selection of my co-authored manuscripts on state-based formal methods tools and applications. A focus lies on the B Method and the animator, constraint solver and model checker ProB.
The first part explores the opportunities that stem from executing state-based specifications. Three approaches are investigated: Firstly, embedding the tool ProB into Java programs and interacting with it using a high-level API that exposes animation, constraint solving and model checking techniques: This technique enables a variety of applications, and has been successfully utilised in a timetable planning tool and a demonstrator in the railway domain. Secondly, treating imperative code as a specification and attempting verification using the model checker CBMC: While technically feasible, verification after implementation comes with a variety of pitfalls and fixing located errors is quite cumbersome at this stage. Finally, embedding the B language into Clojure in order to programmatically generate (parts of) and solve constraints or animate and model check constructed B machines: this approach treats specifications as plain data. Following the ideas of Lisp, this enables tools that analyse and transform specifications as well as the creation of domain-specific languages (DSLs). The second part of this thesis re-visits an implementation of a state space reduction technique, partial order reduction (POR), in ProB. Anecdotally, we had little success with exploiting POR techniques for real-world models. Using a large collection of B machines, we put numbers to our impressions and find that, indeed, in the vast majority of cases, POR does not yield any reduction. Motivated by a grand challenge we set ourselves, — a model of an interlocking system that should be susceptible to POR techniques, yet does not exhibit any reduction — we identify two idioms that hinder POR for higher-level specifications. The first idiom, usage of parameterised operations, often can be eliminated by unrolling a single operation into many, one for each possible parameter value. The second idiom, usage of high-level data structures such as sets or functions, often can be addressed by replacing sets with a bitvector encoding, or using constraint solvers to determine independence of operations. | |||||||
| Lizenz: |  Dieses Werk ist lizenziert unter einer Creative Commons Namensnennung - Nicht kommerziell - Keine Bearbeitungen 4.0 International Lizenz | |||||||
| Fachbereich / Einrichtung: | Mathematisch- Naturwissenschaftliche Fakultät » WE Informatik » Softwaretechnik und Programmiersprachen | |||||||
| Dokument erstellt am: | 30.01.2023 | |||||||
| Dateien geändert am: | 30.01.2023 | |||||||
| Promotionsantrag am: | 12.07.2022 | |||||||
| Datum der Promotion: | 14.10.2022 |
