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\ssen, 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} }