Istituto di Scienza e Tecnologie dell'Informazione     
Ferrari A., Grasso D., Magnani G., Fantechi A., Tempestini M. The Metrô Rio ATP case study. In: FMICS 2010 - Formal Methods for Industrial Critical Systems. 15th International Workshop (Antwerp, Belgium, 20-21 September 2010). Proceedings, pp. 1 - 16. Stefan Kowalewski, Marco Roveri (eds.). (Lecture Notes in Computer Science, vol. 6371). Springer, 2010.
This paper reports on the Simulink/Stateflow based development of the on-board equipment of the Metrô Rio Automatic Train Protection system. Particular focus is given to the strategies followed to address formal weaknesses and certification issues of the adopted tool-suite. On the development side, constraints on the Simulink/Stateflow semantics have been introduced and design practices have been adopted to gradually achieve a formal model of the system. On the verification side, a two-phase approach based on model based testing and abstract interpretation has been followed to enforce functional correctness and runtime error freedom. Quantitative results are presented to assess the overall strategy: the effort required by the design activities is balanced by the effectiveness of the verification tasks enabled by model based development and automatic code generation.
URL: http://www.springerlink.com/content/vh0734j73j8q5002/
DOI: 10.1007/978-3-642-15898-8_1
Subject Formal Methods
Industrial Case Study
Automatic Train Protection
Code Generation
Abstract Interpretation
Model-based Testing
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