The main goal of a railway network operator is to provide a timely and safe train service. Automation and computer driven train control are essential elements towards achieving such a service for large railway systems. Automated Command and Control Systems cover a wide range of functionality in routing, communication and protecting trains in continuous safety-critical operation, interfacing with timetable servers for automatic operation, numerous trackside elements as well as humanmachine-interfaces (HMIs). The overall goal in this use case is to test  novel approaches to verification and validation of large and complex systems with special focus on managing variability and reducing the associated costs for validation by the use of formal methods. The focus of the Complex Automated Command and Control Systems use case will be on:

  • Description of the environment a rail automated command and control system is operated in
  • Description of market and different customer requirements
  • Elaborate a comprehensive set of requirements to allow for test case reduction
  • Prototype implementation of systems and subsystems to be validated
  • Description of security and safety requirements

This demonstrator consists of multiple elements, showing the benefits of formal verification and validation techniques including model based testing. A video on formal modelling and its  benefits for the rail domain is shown, as well as a live demonstration of the Rodin modeling tool and an animation relevant for validation. Moreover, model based testing explaining the complexity of testing safety critical systems is presented, using the example of a railway track, demonstrated at the “Transport Research Arena” Conference 2018 in  mid-April. Additionally, a 3D animated video of this model based testing setup is shown:

  • formal modelling video
  • Rodin live presentation (+ animation)
  • technical video of conference run