Istituto di Scienza e Tecnologie dell'Informazione     
Ferrari A., Fantechi A., Papini M., Grasso D. An industrial application of formal model based development: the Metro Rio ATP case. In: SERENE 2010 - 2nd International Workshop on Software Engineering for Resilient Systems (London, UK, 13-16 April 2010). Proceedings, pp. 71 - 76. ACM, 2010.
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 certifi ed 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 certifi cation issues related to the adopted tool-suite.
Subject Formal Methods
Industrial Case Study
Railway Signaling
D.2.4 Software/Program Verification

Icona documento 1) Download Document PDF

Icona documento Open access Icona documento Restricted Icona documento Private


Per ulteriori informazioni, contattare: Librarian http://puma.isti.cnr.it

Valid HTML 4.0 Transitional