The Metrô Rio ATP case study (Contributo in atti di convegno)

Type
Label
  • The Metrô Rio ATP case study (Contributo in atti di convegno) (literal)
Anno
  • 2010-01-01T00:00:00+01:00 (literal)
Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#doi
  • 10.1007/978-3-642-15898-8_1 (literal)
Alternative label
  • Ferrari A., Grasso D., Magnani G., Fantechi A., Tempestini M. (2010)
    The Metrô Rio ATP case study
    in FMICS 2010 - Formal Methods for Industrial Critical Systems. 15th International Workshop, Antwerp, Belgium, 20-21 September 2010
    (literal)
Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#autori
  • Ferrari A., Grasso D., Magnani G., Fantechi A., Tempestini M. (literal)
Pagina inizio
  • 1 (literal)
Pagina fine
  • 16 (literal)
Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#url
  • http://www.springerlink.com/content/vh0734j73j8q5002/ (literal)
Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#volumeInCollana
  • 6371 (literal)
Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#note
  • In: FMICS 2010 - Formal Methods for Industrial Critical Systems. 15th International Workshop (Antwerp, Belgium, 20-21 September 2010). Proceedings, pp. 1 - 16. Stefan Kowalewski, Marco Roveri (eds.). (Lecture Notes in Computer Science, vol. 6371). Springer, 2010. (literal)
Note
  • PuMa (literal)
  • Scopu (literal)
  • ISI Web of Science (WOS) (literal)
Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#affiliazioni
  • General Electric Transportation Systems, Firenze, Italy; Università degli Studi di Firenze, Italy; Università degli Studi di Firenze, Italy; CNR-ISTI, Pisa-Università degli Studi di Firenze, Italy; General Electric Transportation Systems, Firenze, Italy (literal)
Titolo
  • The Metrô Rio ATP case study (literal)
Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#isbn
  • 978-3-642-15897-1 (literal)
Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#curatoriVolume
  • Stefan Kowalewski, Marco Roveri (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. 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
Autore CNR
Insieme di parole chiave

Incoming links:


Prodotto
Autore CNR di
Insieme di parole chiave di
data.CNR.it