Designing a deadlock-free train scheduler: A model checking approach (Contributo in atti di convegno)

Type

• Contributo in atti di convegno (Classe)
• Prodotto della ricerca (Classe)

Label

• Designing a deadlock-free train scheduler: A model checking approach (Contributo in atti di convegno) (literal)

Anno

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

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

• 10.1007/978-3-319-06200-6_22 (literal)

Alternative label

• Mazzanti F., Spagnolo G.O., Ferrari A. (2014)
  Designing a deadlock-free train scheduler: A model checking approach
  in NASA Formal Methods. 6th International Symposium, Houston, TX, USA, 29 April - 1 May 2014
  (literal)

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

• Mazzanti F., Spagnolo G.O., Ferrari A. (literal)

Pagina inizio

• 264 (literal)

Pagina fine

• 269 (literal)

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

• Progetto: Train Control Enhancement via Information Technology Acronimo: TRACE-IT Grant agreement: PAR FAS 2007--2013 (literal)

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

• http://www.scopus.com/inward/record.url?eid=2-s2.0-84901685108&partnerID=q2rCbXpz (literal)

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

• 8430 LNCS (literal)

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

• 8430 LNCS (literal)

Rivista

• Lecture notes in computer science (Rivista)

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

• 5 (literal)

Note

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

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

• ISTI-CNR, Pisa, Italy; ISTI-CNR, Pisa, Italy; ISTI-CNR, Pisa, Italy. (literal)

Titolo

• Designing a deadlock-free train scheduler: A model checking approach (literal)

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

• 978-3-319-06200-6 (literal)

Abstract

• In this paper we present the approach used in the design of the scheduling kernel of an Automatic Train Supervision (ATS) system. A formal model of the railway layout and of the expected service has been used to identify all the possible critical sections of the railway layout in which a deadlock might occur. For each critical section, the prevention of the occurrence of deadlocks is achieved by constraining the set of trains allowed to occupy these sections at the same time. The identification of the critical sections and the verification of the correctness of the logic used by the ATS is carried out by exploiting a model checking verification framework locally developed at ISTI-CNR and based on the tool UMC. (literal)

Prodotto di

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

Autore CNR

• ALESSIO FERRARI (Unità di personale interno)
• Giorgio Oronzo Spagnolo (Unità di personale esterno)
• FRANCO MAZZANTI (Unità di personale interno)

Insieme di parole chiave

• Keywords of "Designing a deadlock-free train scheduler: A model checking approach" (Insieme di parole chiave)

Incoming links:

Autore CNR di

• FRANCO MAZZANTI (Unità di personale interno)
• Giorgio Oronzo Spagnolo (Unità di personale esterno)
• ALESSIO FERRARI (Unità di personale interno)

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)

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

• Lecture notes in computer science (Rivista)

Insieme di parole chiave di

• Keywords of "Designing a deadlock-free train scheduler: A model checking approach" (Insieme di parole chiave)