Document - The Metro Rio case study

2013

Journal article Open Access

The Metro Rio case study

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

Abstract Interpretation Code generation Railway Model-based development Software Formal methods

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. Formal verification has been experimented as a side activity of the project. 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: Science of computer programming (Print) 78 (2013): 828. doi:10.1016/j.scico.2012.04.003

Publisher: North-Holland, Amsterdam , Paesi Bassi

Metrics

Back to previous page

Cite as

BibTeX entry

@article{oai:it.cnr:prodotti:315536,
	title = {The Metro Rio case study},
	author = {Ferrari A. and Fantechi A. and Magnani G. and Grasso D. and Tempestini M.},
	publisher = {North-Holland, Amsterdam , Paesi Bassi},
	doi = {10.1016/j.scico.2012.04.003},
	journal = {Science of computer programming (Print)},
	volume = {78},
	pages = {828},
	year = {2013}
}