Model checking interlocking control tables (Contributo in atti di convegno)

Type
Label
  • Model checking interlocking control tables (Contributo in atti di convegno) (literal)
Anno
  • 2011-01-01T00:00:00+01:00 (literal)
Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#doi
  • 10.1007/978-3-642-14261-1_11 (literal)
Alternative label
  • Ferrari A., Magnani G., Grasso D., Fantechi A. (2011)
    Model checking interlocking control tables
    in Formal Methods for Automation and Safety in Railway and Automotive Systems 2010 - FORMS/FORMAT 2010, Braunschweig, Germany, 2-3 December 2010
    (literal)
Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#autori
  • Ferrari A., Magnani G., Grasso D., Fantechi A. (literal)
Pagina inizio
  • 107 (literal)
Pagina fine
  • 115 (literal)
Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#altreInformazioni
  • ISBN online: 978-3-642-14261-1 ; ID Modulo Commessa 4147 - ICT.P09.008.002 - 074 - Metodi e Strumenti per la Progettazione di Sistemi Software-Intensive ad Elevata Complessità ; Area di valutazione 01 - Scienze matematiche e informatiche Ferrari, Alessio ; Magnani, Gianluca ; Grasso, Daniele ; Fantechi, Alessandro (literal)
Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#url
  • http://www.springerlink.com/content/j5318h232646410w/ (literal)
Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#titoloVolume
  • FORMS/FORMAT 2010 : Formal Methods for Automation and Safety in Railway and Automotive Systems, vol. 2 (literal)
Note
  • Scopu (literal)
  • PuMa (literal)
Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#affiliazioni
  • General Electric Transportation Systems ; Università degli Studi di Firenze ; CNR-ISTI, Pisa, Italy (literal)
Titolo
  • Model checking interlocking control tables (literal)
Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#isbn
  • 978-3-642-14260-4 (literal)
Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#curatoriVolume
  • Eckehard Schnieder, Geza Tarnai (literal)
Abstract
  • A challenging problem for model checking is represented by railway interlocking systems. It is a well known fact that interlocking systems, due to their inherent complexity related to the high number of variables involved, are not amenable to automatic verifi cation, typically incurring in state space explosion problems. The literature is however quite scarce on data concerning the size of interlocking systems that have been successfully proved with model checking techniques. In this paper we attempt a systematic study of the applicability bounds for general purpose model checkers on this class of systems, by studying the typical characteristics of control tables and their size parameters. The results con firm that, although small scale interlocking systems can be addressed by model checking, interlockings that control medium or large railway yards cannot, asking for specialized verifi cation techniques. (literal)
Editore
Prodotto di
Autore CNR
Insieme di parole chiave

Incoming links:


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