(M) Modelling and Verification of a Model Railway

The Software Technologies Research Group (SWT) has built a digital model railway (SWTbahn [1–2]) for use in teaching. SWTbahn consists of hardware tracks, signals, points, and trains, and software for monitoring and controlling railway routes and trains. It gives students a realistic case study to support their learning of important principles in the design, programming, and verification of safety-critical systems. In particular, students can design algorithms to schedule trains and manage train routes, and have them automatically verified, e.g., by a model checker such as nuXmv. Such verification, however, requires certain aspects of SWTbahn to be captured in a computer-readable model.

This thesis shall:   
(i) Investigate state-of-the-art modelling techniques for railway systems in the context of verification (e.g., [3]) and their applicability to the SWTbahn;   
(ii) Design and develop models for core aspects of SWTbahn (e.g., railway network, signalling, and trains) based on SWTbahn documentation and configuration files;   
(iii) Apply formal verification tools (e.g., [4-5]) to verify safety properties of the developed models.

The ideal student for this thesis topic will have a keen interest in modeling and formal verification. Knowledge in formal verification tools, e.g., acquired in the module Applied Software Verification (SWT-ASV-M), 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 17 January 2023).
2. Prototype tool for controlling trains using BiDiB. Available at https://github.com/uniba-swt/swtbahn-cli (last accessed on 17 January 2023).
   
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, 10.1007/s10009-014-0304-7, 2014.
4. R. Cavada, A. Cimatti, M. Dorigatti, A. Griggio, A. Mariotti, A. Micheli, S. Mover, M. Roveri, and S. Tonetta. The nuxmv symbolic model checker. In Computer Aided Verification (CAV 2014), volume 8559 of Lecture Notes in Computer Science, pages 334–342. Springer, 2014.
5. A. Cimatti, E. M. Clarke, E. Giunchiglia, F. Giunchiglia, M. Pistore, M. Roveri, R. Sebastiani, and A. Tacchella. NuSMV 2: An OpenSource Tool for Symbolic Model Checking. In Computer Aided Verification (CAV 2002), volume 2404 of Lecture Notes in Computer Science, pages 359–364. Springer, 2002.