(B|M) SWTbahn Interlocker: Railway Interlocking System

The Software Technologies Research Group (SWT) has built a digital model railway (SWTbahn [1–2]) for use in teaching. It gives students a realistic case study to support their learning of important principles in the design, programming, and verification of safety-critical systems. This thesis topic concerns the development of software to accept route requests from train drivers, and to grant their requests by applying interlocking procedures [3].

This thesis shall evaluate an existing prototype [4] of the interlocking system for its capabilities, performance, and safety, and shall extend the prototype in several aspects: (a) handling of train engines with attached carriages or wagons; (b) prioritising the granting of multiple route requests; (c) optimising the employed algorithms and data structures for real-time performance; and (d) creating test cases to demonstrate the correctness of the extended interlocking system. The BahnDSL domain-specific language shall be used to model and implement the model railway track layout and interlocking procedures. Additionally, the interlocking system's interface with the SWTbahn server may need to be updated. For students interested in a Master thesis, this topic shall include the formal verification of the interlocking system against, e.g., potential deadlock situations and safety violations.

The ideal student for this thesis topic will have a keen interest in practical programming, embedded systems, and high confidence systems. Knowledge in C programming would be advantageous. Missing knowledge in some areas or technologies can be acquired during the thesis.

1. Low-level digital control library (BiDiB). Available at https://github.com/uniba-swt/libbidib (last accessed on 15 May 2022).
2. Prototype tool for controlling trains using BiDiB. Available at https://github.com/uniba-swt/swtbahn-cli (last accessed on 15 May 2022).
   
3. P. James, F. Moller, H. N. Nguyen, M. Roggenbach, S. Schneider, and H. Treharne. Techniques for modelling and verifying railway interlockings. International Journal on Software Tools for Technology Transfer, 16(6):683-711, 2014.
   
4. J. Amling. SWTbahn: Safe Operation and Control of a Digital Model Railway. Student Project SWT-PR1-B, WiSe 2018/19, The University of Bamberg.
5. Nguyen, N.T. BahnDSL: A Domain-Specific Language for Configuring and Controlling Railways. Master's thesis, WiSe 2019/20, The University of Bamberg, Germany. Tool available online at https://github.com/trinnguyen/bahndsl (last accessed 15 May 2022).