Mark Bouwman: A model-based test platform for rail signalling systems

Event Details

As technology progresses, newer, and more complex, solutions are employed to verify that rail signalling systems are safe. Formal methods provide ways to increase rigour in the verification process. This precision, accompanied by the ongoing increase of computational power of computers, also opens up ways to partially automate parts of the verification process. We present a case study an application of mCRL2 and the model-based testing tool JTorX in the signalling domain. The mCRL2 toolkit is used to formally model the behaviour of a system at the core of signalling solutions: the interlocking. The behaviour of the interlocking is validated through model checking, proving that relevant safety properties hold. Using JTorX, the formal model is turned into the benchmark in an automated testing platform for interlocking software. A working setup with actual interlocking software on a pre-existing testing platform is presented, though performance and stability remain an issue. The suitability of mCRL2 and JTorX in the signalling domain is evaluated and suggestions are given for improvement and further research.