(B|M) SWTbahn Safety and Compliance

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. Currently, users are responsible for ensuring the safe and correct operation of the model railway, e.g., avoiding train collisions, respecting track signals, and ensuring that points are in their correct positions.

This thesis shall develop a software framework that automates the checking of the SWTbahn platform state and intervenes when an unsafe situation or unapproved action occurs. The platform state can be checked roughly at two different levels: the system level that interfaces directly with the low-level BiDiB [1] hardware (e.g., track segments, trains, points, and signals), and the business level that executes the business logic required for client-server [2] interactions (e.g., managing train routes and movements, enforcing speed limits and track signals, managing users, and (de-)allocating railway resources to users). The framework shall carefully trade-off the prevention and detection of unsafe situations, provide a means to prioritise and handle a set of unsafe situations, execute non-invasive remedies, while at the same time enhance how the platform state is stored and retrieved, and how feedback is provided to the user and logging system.

This thesis topic is suitable for Masters students, and it is also suitable for Bachelor students by only focusing on the system level in the framework. Computer science Masters students shall additionally use a model checker [3] to statically verify safety requirements as far as possible. The ideal student for this thesis topic will have a keen interest in practical programming, embedded systems, and high confidence systems. Knowledge in C 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 29 Mar 2021).
2. Prototype tool for controlling trains using BiDiB. Available at https://github.com/uniba-swt/swtbahn-cli (last accessed on 29 Mar 2021).
   
3. The nuXmv model checker. Available at https://nuxmv.fbk.eu (last accessed on 29 Mar 2021).