The Metro Rio case study (Articolo in rivista)

Type

• Articolo in rivista (Classe)
• Prodotto della ricerca (Classe)

Label

• The Metro Rio case study (Articolo in rivista) (literal)

Anno

• 2013-01-01T00:00:00+01:00 (literal)

Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#doi

• 10.1016/j.scico.2012.04.003 (literal)

Alternative label

• Ferrari A., Fantechi A., Magnani G., Grasso D., Tempestini M. (2013)
  The Metro Rio case study
  in Science of computer programming (Print)
  (literal)

Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#autori

• Ferrari A., Fantechi A., Magnani G., Grasso D., Tempestini M. (literal)

Pagina fine

• 828 (literal)

Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#altreInformazioni

• [Online First 25 April 2012] (literal)

Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#url

• http://www.sciencedirect.com/science/article/pii/S0167642312000676 (literal)

Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#numeroVolume

• 78 (literal)

Rivista

• Science of computer programming (Rivista)

Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#pagineTotali

• 842 (literal)

Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#numeroFascicolo

• 7 (literal)

Note

• PuMa (literal)
• ISI Web of Science (WOS) (literal)
• Scopu (literal)

Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#affiliazioni

• DSI Dipartimento di Sistemi e Informatica, Universitá di Firenze, Firenze, Italy; DSI Dipartimento di Sistemi e Informatica, Universitá di Firenze, Firenze, Italy; General Electric Transportation Systems, Firenze, Italy; General Electric Transportation Systems, Firenze, Italy; General Electric Transportation Systems, Firenze, Italy; (literal)

Titolo

• The Metro Rio case study (literal)

Abstract

• 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. (literal)

Prodotto di

• Istituto di scienza e tecnologie dell'informazione \"Alessandro Faedo\" (ISTI) (Istituto)
• Metodi e Strumenti per la Progettazione di Sistemi Software-Intensive ad Elevata Complessità (ICT.P09.008.002) (Modulo)

Autore CNR

• ALESSANDRO FANTECHI (Persona)
• ALESSIO FERRARI (Unità di personale interno)

Insieme di parole chiave

• Keywords of "The Metro Rio case study" (Insieme di parole chiave)

Incoming links:

Prodotto

• Istituto di scienza e tecnologie dell'informazione \"Alessandro Faedo\" (ISTI) (Istituto)
• Metodi e Strumenti per la Progettazione di Sistemi Software-Intensive ad Elevata Complessità (ICT.P09.008.002) (Modulo)

Autore CNR di

• ALESSANDRO FANTECHI (Persona)
• ALESSIO FERRARI (Unità di personale interno)

Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#rivistaDi

• Science of computer programming (Rivista)

Insieme di parole chiave di

• Keywords of "The Metro Rio case study" (Insieme di parole chiave)