Document - The Metrô Rio ATP case study

2010

Conference article Restricted

The Metrô 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 Metrô 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.

Metrics

Back to previous page

Cite as

BibTeX entry

@inproceedings{oai:it.cnr:prodotti:44408,
	title = {The Metrô 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},
	year = {2010}
}