An industrial application of formal model based development: the Metro Rio ATP case

The railway and metro signaling industries are currently investigating strategies for the introduction of formal model based development within their development processes. Among the various platforms supporting this technology, the Simulink/Stateflow tool-suite has been adopted in various safety-critical domains for modeling and code generation of controlsystems. Despite their flexibility and ease of use, introduction of these tools for developing dependable software, and in particular signaling applications, has been often hampered by the lack of a rigorous formal semantic sand by the absence of a certified code generator. This paper reports on the Simulink/Stateflow based development of the on-board equipment of the Metro Rio Automatic Train Protection system, describing the design strategy and the approach followed in addressing weaknesses and certification issues related to the adopted tool-suite.