An industrial application of formal model based development: the Metro Rio ATP case
Ferrari A., Fantechi A., Papini M., Grasso D.
Software/Program Verification Formal Methods SOFTWARE ENGINEERING Industrial Case Study Simulink
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 certified 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 certification issues related to the adopted tool-suite.
Source: 2nd International Workshop on Software Engineering for Resilient Systems, pp. 71–76, London, UK, 13-16 April 2010
Publisher: ACM Press, New York, USA
[2] Mathworks Automotive Advisory Board (MAAB), Control Algorithm Modeling Guidelines Using Matlab, Simulink and State ow, Version 2.0, 2007.
[3] S. Bacherini, A. Fantechi, M. Tempestini, and N. Zingoni. A story about formal methods adoption by a railway signaling manufacturer. Proceedings of FM 2006, LNCS, 4025, 2006.
[4] A. Faivre and P. Benoit. Safety critical software of meteor developed with the B formal method and vital coded processor. In Proceedings of WCRR99, pages 84{89, 1999.
[5] A. Ferrari, A. Fantechi, S. Bacherini, and N. Zingoni. Modeling guidelines for code generation in the railway signaling context. In Proceedings of 1st NASA Formal Methods Symphosium. NASA, April 2009.
[6] D. Grasso, A. Fantechi, and A. Ferrari. Model based testing and abstract interpretation in the railway signaling context. In Proceedings of the 3rd International Conference on Software Testing, Veri cation and Validation (to appear), 2010.
[7] G. Hamon. A denotational semantics for state ow. In Proceedings of the 5th ACM international conference on Embedded software, pages 164{172, 2005.
[8] G. Hamon and J. Rushby. An operational semantics for state ow. STTT, 9(5-6):477{456, 2007.
[9] D. Harel. Statecharts: A visual formalism for complex systems. Science of Computer Programming, 8(3):231{274, 1987.
[10] M. Leuschel, J. Falampin, F. Fabian, and D. Plagge. Automated property veri cation for large scale B models. Proceedings of FM 2009, LNCS, 5850:810{814, 2009.
[11] N. Scaife, C. Sofronis, P. Caspi, S. Tripakis, and F. Maraninchi. De ning and translating a safe subset of Simulink/State ow into Lustre. In Proceedings of the 4th ACM international conference on Embedded software, pages 259{268, 2004.
[12] J. Woodcock, P. G. Larsen, J. Bicarregui, and J. Fitzgerald. Formal methods: Practice and experience. ACM Computing Surveys, 5(N):1{39, June 2009.
Metrics
Back to previous page
@inproceedings{oai:it.cnr:prodotti:92139,
title = {An industrial application of formal model based development: the Metro Rio ATP case},
author = {Ferrari A. and Fantechi A. and Papini M. and Grasso D.},
publisher = {ACM Press, New York, USA},
doi = {10.1145/2401736.2401744},
booktitle = {2nd International Workshop on Software Engineering for Resilient Systems, pp. 71–76, London, UK, 13-16 April 2010},
year = {2010}
}
0000-0002-4648-4667DOIAlso available from
