The Metrô Rio case study
| Autor: | Daniele Grasso, Alessio Ferrari, Gianluca Magnani, Matteo Tempestini, Alessandro Fantechi |
|---|---|
| Rok vydání: | 2013 |
| Předmět: |
Correctness
Model-based development Programming language business.industry Computer science Formal methods Railway Abstract Interpretation Stateflow Abstract interpretation computer.software_genre Model-based design Code generation Software engineering business Formal verification computer Automatic train protection Software computer.programming_language |
| Zdroj: | Science of computer programming 78 (2013): 828. doi:10.1016/j.scico.2012.04.003 info:cnr-pdr/source/autori:Ferrari A.; Fantechi A.; Magnani G.; Grasso D.; Tempestini M./titolo:The Metro Rio case study/doi:10.1016%2Fj.scico.2012.04.003/rivista:Science of computer programming (Print)/anno:2013/pagina_da:/pagina_a:828/intervallo_pagine:828/volume:78 |
| ISSN: | 0167-6423 |
| DOI: | 10.1016/j.scico.2012.04.003 |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full Text from ScienceDirect