The Community for Technology Leaders
RSS Icon
Issue No.03 - May-June (2013 vol.30)
pp: 28-34
Alessio Ferrari , CNR-ISTI
Alessandro Fantechi , Università di Firenze
Stefania Gnesi , CNR-ISTI
Gianluca Magnani , General Electric Transportation Systems, Florence
The transition from a code-based process to a model-based process isn't easy. This is particularly true for a company that operates in a safety-critical sector, where the products must be developed according to international standards, with certified tools and controlled processes. The authors summarize the experience of a railway signaling manufacturer that decided to adopt general-purpose, model-based tools—namely, Simulink/Stateflow and SysML—for product development. The company faced challenges primarily concerning the verification of the software and the integration of the tools within the existing process. Structured development solutions and formal/semiformal approaches were adopted to tackle the challenges.
Modeling, Software packages, Encoding, Rail transportation, Standards, System analysis and design, Safety, programming paradigms, software engineering process, formal methods, software and system safety
Alessio Ferrari, Alessandro Fantechi, Stefania Gnesi, Gianluca Magnani, "Model-Based Development and Formal Methods in the Railway Industry", IEEE Software, vol.30, no. 3, pp. 28-34, May-June 2013, doi:10.1109/MS.2013.44
1. J. Woodcock et al., “Formal Methods: Practice and Experience,” ACM Computing Surveys, vol. 41, no. 4, pp. 19:1–19:36.
2. S. Bacherini et al., “A Story about Formal Methods Adoption by a Railway Signaling Manufacturer,” Proc. 14th Int'l Symp. Formal Methods, LNC S 4085, Springer, 2006, pp. 179–189.
3. D. Harel, “Statecharts: A Visual Formalism for Complex Systems,” Science Computer Programming, vol. 8, no. 3, 1987, pp. 231–274.
4. A. Ferrari et al., “The Metrô Rio Case Study,” to be published in Science Computer Programming, 2013; doi: 10.1016/j.scico.2012.04.003.
5. A. Ferrari et al., “Modeling Guidelines for Code Generation in the Railway Signaling Context,” Proc. 1st NASA Formal Methods Symp., NASA, 2009, pp. 166–170.
6. N. Scaife et al., “Defining and Translating a 'Safe' Subset of Simulink/Stateflow into Lustre,” Proc. 4th ACM Int'l Conf. Embedded Software, ACM, 2004, pp. 259–268.
7. M. Conrad, “Testing-Based Translation Validation of Generated Code in the Context of IEC 61508,” Formal Methods in System Design, vol. 35, no. 3, 2009, pp. 340–389.
8. P. Cousot and R. Cousot, “Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints,” Proc. 4th ACM SIGACT-SIGPLAN Symp. Principles of Programming Languages, ACM, 1977, pp. 238–252.
9. A. Ferrari et al., “Adoption of Model-Based Testing and Abstract Interpretation by a Railway Signaling Manufacturer,” Int'l J. Embedded and Real-Time Communication Systems, vol. 2, no. 2, 2011, pp. 42–61.
10. A.J. Kornecki and J. Zalewski, “Certification of Software for Real-Time Safety-Critical Systems: State of the Art,” Innovations in Systems and Software Eng., vol. 5, no. 2, 2009, pp. 149–161.
6 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool