This paper reports on the Simulink/Stateflow based development of the on-board equipment of the Metro Rio Automatic Train Protection system. Particular focus is given to the strategies followed to address formal weaknesses and certification issues of the adopted toolsuite. 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.

The Metro Rio ATP case study / A. Ferrari; D. Grasso; G. Magnani; A. Fantechi. - STAMPA. - Lecture Notes in Computer Science 6371:(2010), pp. 1-16. (Intervento presentato al convegno 15th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2010) tenutosi a Antwerp, Belgio nel Settembre).

The Metro Rio ATP case study

FERRARI, ALESSIO;GRASSO, DANIELE;MAGNANI, GIANLUCA;FANTECHI, ALESSANDRO
2010

Abstract

This paper reports on the Simulink/Stateflow based development of the on-board equipment of the Metro Rio Automatic Train Protection system. Particular focus is given to the strategies followed to address formal weaknesses and certification issues of the adopted toolsuite. 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.
2010
15th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2010)
Antwerp, Belgio
Settembre
A. Ferrari; D. Grasso; G. Magnani; A. Fantechi
File in questo prodotto:
File Dimensione Formato  
FMICS10.pdf

Accesso chiuso

Tipologia: Versione finale referata (Postprint, Accepted manuscript)
Licenza: Tutti i diritti riservati
Dimensione 3.3 MB
Formato Adobe PDF
3.3 MB Adobe PDF   Richiedi una copia

I documenti in FLORE sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificatore per citare o creare un link a questa risorsa: https://hdl.handle.net/2158/395967
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 12
  • ???jsp.display-item.citation.isi??? 5
social impact