Distributing the challenge of model checking interlocking control tables (Contributo in atti di convegno)

Type
Label
  • Distributing the challenge of model checking interlocking control tables (Contributo in atti di convegno) (literal)
Anno
  • 2012-01-01T00:00:00+01:00 (literal)
Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#doi
  • 10.1007/978-3-642-34032-1_26 (literal)
Alternative label
  • Fantechi A. (2012)
    Distributing the challenge of model checking interlocking control tables
    in Leveraging Applications of Formal Methods, Verification and Validation. Applications and Case Studies - 5th International Symposium, Heraclion, Crete, 15-18 October 2012
    (literal)
Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#autori
  • Fantechi A. (literal)
Pagina inizio
  • 276 (literal)
Pagina fine
  • 289 (literal)
Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#url
  • http://www.springerlink.com/content/f17j73125w645123/ (literal)
Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#titoloVolume
  • Lecture Notes in Computer Science (literal)
Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#volumeInCollana
  • 7610 (literal)
Note
  • PuMa (literal)
  • Scopu (literal)
Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#affiliazioni
  • CNR-ISTI, Pisa, Italy; (literal)
Titolo
  • Distributing the challenge of model checking interlocking control tables (literal)
Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#isbn
  • 978-3-642-34031-4 (literal)
Abstract
  • Railway interlocking systems represent a challenge for model checkers: although encoding interlocking rules as finite state machines can be quite straightforward, and safety properties to be proved are easily expressible, the inherent complexity related to the high number of variables involved makes the verification of such systems typically incur state space explosion problems. Domain-specific techniques have been adopted to advance the size of interlocking systems that can be successfully proved, but still not reaching the size needed for large deployment cases. We propose a novel approach in which we exploit a distributed modelling of an interlocking system and a careful selection of verification scenarios, so that parallel verifications conducted on multiple processors can address systems of a large size. Some experiments in this direction are presented and new directions of research according to this proposal are discussed. (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