Dokument: Modellierung und Verifikation von Eisenbahnsystemen: Übersetzung von RailML in die B-Methode
| Titel: | Modellierung und Verifikation von Eisenbahnsystemen: Übersetzung von RailML in die B-Methode | |||||||
| Weiterer Titel: | Modeling and Verification of Railway Systems: Translation of RailML Into the B-Method | |||||||
| URL für Lesezeichen: | https://docserv.uni-duesseldorf.de/servlets/DocumentServlet?id=66002 | |||||||
| URN (NBN): | urn:nbn:de:hbz:061-20241007-160441-4 | |||||||
| Kollektion: | Publikationen | |||||||
| Sprache: | Englisch | |||||||
| Dokumententyp: | Wissenschaftliche Abschlussarbeiten » Studienabschlussarbeit (z.B. Bachelor-, Master-, Examensarbeit) | |||||||
| Medientyp: | Text | |||||||
| Autor: | Gruteser, Jan [Autor] | |||||||
| Dateien: |
| |||||||
| Beitragende: | Prof. Dr. Leuschel, Michael [Gutachter] Dr. Bendisposto, Jens [Gutachter] | |||||||
| Dewey Dezimal-Klassifikation: | 000 Informatik, Informationswissenschaft, allgemeine Werke » 004 Datenverarbeitung; Informatik | |||||||
| Beschreibung: | The aim of this work is to translate files written in railML to the formal B-method to enable formal verification and validation of the specifications. RailML is an XML-based format designed to facilitate the exchange of information about railway systems between railway applications. Since undetected small errors in the modelling can lead to serious errors in the real system, especially with safety-critical properties such as train protection, the files should always be subjected to an automatic validation.
The approach developed in this thesis allows automatic syntactic and semantic validation against predefined rules. For this purpose, ProB and its integrated B-Rules DSL are used to validate these rules. In addition to the validation, a B-model is presented to animate the behaviour of the specification, which can also be used for simulations and statistical tests using SimB. By using generated machines, the user can also define custom rules for validation using the mathematical expressiveness of the B language. A strategy for creating visualisations of the topology using Graphviz is presented, which can also be used with VisB to visualise the current state. The entire process is made available in a user-friendly way through integration into the ProB2-UI. Finally, case studies are investigated to show that the implemented validation process can be efficiently applied to complex models and that errors can be successfully detected in some of the models. | |||||||
| Lizenz: |  Dieses Werk ist lizenziert unter einer Creative Commons Namensnennung 4.0 International Lizenz | |||||||
| Fachbereich / Einrichtung: | Mathematisch- Naturwissenschaftliche Fakultät » WE Informatik » Softwaretechnik und Programmiersprachen | |||||||
| Dokument erstellt am: | 07.10.2024 | |||||||
| Dateien geändert am: | 07.10.2024 |
