FLORE (FLOrence REsearch) è il repository istituzionale ad accesso pieno e aperto dell'Università degli Studi di Firenze.
Raccoglie, documenta e conserva le informazioni sulla produzione scientifica dell'Università e costituisce l'Anagrafe della ricerca dell'Ateneo.
EnglishThis 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.
| Titolo: | The Metro Rio ATP case study | |
| Autori di Ateneo: | ||
| Autori: | FERRARI, ALESSIO; GRASSO, DANIELE; MAGNANI, GIANLUCA; FANTECHI, ALESSANDRO | |
| Data di pubblicazione: | 2010 | |
| Titolo del congresso: | 15th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2010) | |
| Luogo del congresso: | Antwerp, Belgio | |
| Data del congresso: | Settembre | |
| 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. | |
| Handle: | http://hdl.handle.net/2158/395967 | |
| Appare nelle tipologie: | 4a - Articolo in atti di congresso |
File in questo prodotto:
| File | Descrizione | Tipologia | Licenza | |
|---|---|---|---|---|
| FMICS10.pdf | Versione finale referata (Postprint, Accepted manuscript) | DRM non definito | Administrator Richiedi una copia |
http://hdl.handle.net/2158/395967
Copyright © 2022