Formal Design and Validation of an Automatic Train Operation Control System

In this paper, we report on the design of a complex control system, namely the Automatic Train Operation (ATO), which aims at enhancing the Grade of Automation in train operations (passenger transportation, infrastructure monitoring) in high-speed lines. The development of ATO is being conducted as an industrial project, with contributions from different research teams. The design of the system is complex in terms of architecture, functionality, safety and reliability requirements to be fulfilled, and geographical distribution of the development teams. Formal methods and model-based design are used to master the complexity of the design and of the system integration. Our approach is based on formal tools for system specification and validation, which support automatic code generation, early design validation, testing and simulation, and runtime verification. Moreover, we structured the development process in different phases and configurations, corresponding to increasing functionality of the system and different deployment configurations. The project is at an advanced stage of execution. In this paper, we demonstrate the effectiveness of the proposed approach and methodology, we discuss our experience and the lessons learned.