Abstract
Stellwerke stellen eine zentrale Komponente fu¨r den sicheren Schienenverkehr dar. Um die korrekte Funktionsweise sicherzustellen und sicherheitskritische Zust¨ande auszuschließen, sind formale Methoden angebracht.
In dieser Arbeit soll gezeigt werden, wie in der Modellierungssprache SAML (Sys-tem Analaysis and Modeling Language) ein Baukastensystem erstellt wird, mit dem sich beliebige Stellwerke modellieren lassen. In Rahmen der Arbeit wird beschrie-ben, wie das reale System abstrahiert wurde, um das zu untersuchende Verhal-ten herauszustellen. Die Arbeit beschreibt weiterhin die Sicherheits- und Liveness-Spezifikationen, die zur Verifikation der generierten Bahnhofsstellwerke genutz wer-den. Im Anschluss wird an einem Beispiel die Modellierung eines Bahnhofsstellwerkes auf Basis des vorgestellten Baukastensystems gezeigt. Bei der Verifikation wurde ei-ne kleine Auswahl an Model-Checking-Tools genutzt. Ein Vergleich dieser Tools in Bezug auf das hier gestellte Problem sowie eine Auswertung der Erfahrungen, die w¨ahrend des Projektes gesammelt werden konnten, sollen den Abschluss bilden.
Links
BibTeX (Download)
@mastersthesis{Bedau2017,
title = {Modellbasierte Sicherheitsanalyse eines Bahnhofsstellwerks},
author = {Ludwig Bedau},
editor = {Otto-von-Guericke-Universit\"{a}t Magdeburg},
url = {https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2018/02/BA_2017_BedauLudwig.pdf},
year = {2017},
date = {2017-03-31},
school = {Otto-von-Guericke-Universit\"{a}t Magdeburg},
abstract = {Stellwerke stellen eine zentrale Komponente fu¨r den sicheren Schienenverkehr dar. Um die korrekte Funktionsweise sicherzustellen und sicherheitskritische Zust¨ande auszuschlie{\ss}en, sind formale Methoden angebracht.
In dieser Arbeit soll gezeigt werden, wie in der Modellierungssprache SAML (Sys-tem Analaysis and Modeling Language) ein Baukastensystem erstellt wird, mit dem sich beliebige Stellwerke modellieren lassen. In Rahmen der Arbeit wird beschrie-ben, wie das reale System abstrahiert wurde, um das zu untersuchende Verhal-ten herauszustellen. Die Arbeit beschreibt weiterhin die Sicherheits- und Liveness-Spezifikationen, die zur Verifikation der generierten Bahnhofsstellwerke genutz wer-den. Im Anschluss wird an einem Beispiel die Modellierung eines Bahnhofsstellwerkes auf Basis des vorgestellten Baukastensystems gezeigt. Bei der Verifikation wurde ei-ne kleine Auswahl an Model-Checking-Tools genutzt. Ein Vergleich dieser Tools in Bezug auf das hier gestellte Problem sowie eine Auswertung der Erfahrungen, die w¨ahrend des Projektes gesammelt werden konnten, sollen den Abschluss bilden.},
keywords = {interlocking systems, Railway System Verification},
pubstate = {published},
tppubtype = {mastersthesis}
}