Document - The Metrô Rio ATP case study

2010

Conference article Restricted

The Metrô Rio ATP case study

Ferrari A., Grasso D., Magnani G., Fantechi A., Tempestini M.

Software/Program Verification Formal Methods Automatic Train Protection SOFTWARE ENGINEERING Industrial Case Study

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.

Source: FMICS 2010 - Formal Methods for Industrial Critical Systems. 15th International Workshop, pp. 1–16, Antwerp, Belgium, 20-21 September 2010

Metrics

Back to previous page

Cite as

BibTeX entry

@inproceedings{oai:it.cnr:prodotti:44408,
	title = {The Metrô Rio ATP case study},
	author = {Ferrari A. and Grasso D. and Magnani G. and Fantechi A. and Tempestini M.},
	doi = {10.1007/978-3-642-15898-8_1},
	booktitle = {FMICS 2010 - Formal Methods for Industrial Critical Systems. 15th International Workshop, pp. 1–16, Antwerp, Belgium, 20-21 September 2010},
	year = {2010}
}