Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
European Committee for Electrotechnical Standardization: CENELEC EN 50128, Railway Applications - Software for Railway Control and Protection Systems (1997)
Ferrari, A., Fantechi, A., Bacherini, S., Zingoni, N.: Modeling Guidelines for Code Generation in the Railway Signaling Context. In: 1st NASA Formal Methods Symphosium (NFM), Moffet Field, California, U.S.A. (2009)
Harel, D.: Statecharts: A Visual Formalism for Complex Systems. Science of Computer Programming 8(3), 231–274 (1987)
Hamon, G., Rushby, J.: An operational semantics for stateflow. In: Wermelinger, M., Margaria-Steffen, T. (eds.) FASE 2004. LNCS, vol. 2984, pp. 229–243. Springer, Heidelberg (2004)
Hamon, G.: A denotational semantics for stateflow. In: 5th ACM Int. Conf. on Embedded Software, Jersey City, NJ, USA, pp. 164–172 (2005)
Mathworks Automotive Advisory Board (MAAB): Control Algorithm Modeling Guidelines Using Matlab, Simulink and Stateflow, Version 2.0 (2007), http://www.mathworks.com/industries/auto/maab.html
Sahbani, A., Pascal, J.C.: Simulation of hybrid systems using stateflow. In: Proceedings of the 14th European Simulation Multiconference on Simulation and Modelling: Enablers for a Better Quality of Life, pp. 271–275 (2000)
Scaife, N., et al.: Defining and translating a safe subset of simulink/stateflow into lustre. In: 4th ACM Int. Conf. on Embedded Software, Pisa, Italy, pp. 259–268 (2004)
Bacherini, S., Fantechi, A., Tempestini, M., Zingoni, N.: A Story about Formal Methods Adoption by a Railway Signaling Manufacturer. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol. 4085, pp. 179–189. Springer, Heidelberg (2006)
Conrad, M.: Testing-based translation validation of generated code in the context of IEC 61508. In: Formal Methods in System Design, pp. 389–401. Springer, Heidelberg (2009)
Baresel, A., Conrad, M., Sadeghipour, S., Wegener, J.: The interplay between model coverage and code coverage. In: Proceedings of the 11th Eur. int. Conf. on Software Testing, Analysis and Review EuroSTAR’03, Amsterdam, Netherlands (2003)
Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: 4th ACM Symp. on Principles of Programming Languages (POPL), Los Angeles, California, pp. 238–252 (1977)
Grasso, D., Fantechi, A., Ferrari, A.: Model Based Testing and Abstract Interpretation in the Railway Signaling Context. In: 3rd International Conference on Software Testing, Verification and Validation (ICST), Paris, France, pp. 103–106 (2010)
Deutsch, A.: Static verification of dynamic properties. PolySpace White Paper (2004)
Ferrari, A., Fantechi, A., Papini, M., Grasso, D.: An industrial application of formal model based development: the Metrô Rio ATP case. In: 2nd International Workshop on Software Engineering for Resilient Systems, SERENE 2010 (2010)
Faivre, A., Benoit, P.: Safety critical software of meteor developed with the B formal method and vital coded processor. In: Proc. of WCRR’99, pp. 84–89 (1999)
Guiho, G., Hennebert, A.: SACEM Software Validation. In: 12th International Conference on Software Engineering, pp. 186–191 (1990)
Leuschel, M., et al.: Automated property verification for large scale B models. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol. 5850, pp. 810–814. Springer, Heidelberg (2009)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ferrari, A., Grasso, D., Magnani, G., Fantechi, A., Tempestini, M. (2010). The Metrô Rio ATP Case Study. In: Kowalewski, S., Roveri, M. (eds) Formal Methods for Industrial Critical Systems. FMICS 2010. Lecture Notes in Computer Science, vol 6371. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-15898-8_1
Download citation
DOI: https://doi.org/10.1007/978-3-642-15898-8_1
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-15897-1
Online ISBN: 978-3-642-15898-8
eBook Packages: Computer ScienceComputer Science (R0)