PUMA
Istituto di Scienza e Tecnologie dell'Informazione     
Ferrari A., Fantechi A., Magnani G., Grasso D., Tempestini M. The Metro Rio case study. In: Science of Computer Programming, vol. 78 (7) pp. 828 - 842. Elsevier, 2013.
 
 
Abstract
(English)
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.
URL: http://www.sciencedirect.com/science/article/pii/S0167642312000676
DOI: 10.1016/j.scico.2012.04.003
Subject Formal methods
Abstract Interpretation, ,
Model-based development
Code generation
Railway
Model-based testing
Model checking
Theorem proving
Prover
Polyspace
D.2 SOFTWARE ENGINEERING
D.2.1 Requirements/Specifications
D.2.2 Design Tools and Techniques
D.2.3 Coding Tools and Techniques
D.2.4 Software/Program Verification. Model checking


Icona documento 1) Download Document PDF
Icona documento 2) Download Document PDF


Icona documento Open access Icona documento Restricted Icona documento Private

 


Per ulteriori informazioni, contattare: Librarian http://puma.isti.cnr.it

Valid HTML 4.0 Transitional