In this paper we present the deadlock avoidance approach used in the design of the scheduling kernel of an Automatic Train Supervision (ATS) system. The ATS that we have designed prevents the occurrence of deadlocks by performing a set of runtime checks just before allowing a train to move further. For each train, the set of checks to be performed at each step of progress is retrieved from statically generated ATS configuration data. For the verification of the correctness of the logic used by the ATS and the validation of the constraints verified by the runtime checks, we define a formal model that represents the ATS behavior, the railway layout, and the planned service structure. We use this formal model to verify both the absence of deadlocks and absence of false positives (i.e., cases in which a train is unnecessarily disallowed to proceed). The verification is carried out by exploiting the UMC model checking verification framework locally developed at ISTI-CNR.

Deadlock Avoidance in Train Scheduling: A Model Checking Approach / Franco Mazzanti;Giorgio Oronzo Spagnolo;Simone Della Longa;Alessio Ferrari. - ELETTRONICO. - 8718:(2014), pp. 109-123. (Intervento presentato al convegno 19th International Conference on Formal Methods for Industrial Critical Systems tenutosi a Florence; Italy nel 11-12 September 2014) [10.1007/978-3-319-10702-8_8].

Deadlock Avoidance in Train Scheduling: A Model Checking Approach

SPAGNOLO, GIORGIO ORONZO;FERRARI, ALESSIO
2014

Abstract

In this paper we present the deadlock avoidance approach used in the design of the scheduling kernel of an Automatic Train Supervision (ATS) system. The ATS that we have designed prevents the occurrence of deadlocks by performing a set of runtime checks just before allowing a train to move further. For each train, the set of checks to be performed at each step of progress is retrieved from statically generated ATS configuration data. For the verification of the correctness of the logic used by the ATS and the validation of the constraints verified by the runtime checks, we define a formal model that represents the ATS behavior, the railway layout, and the planned service structure. We use this formal model to verify both the absence of deadlocks and absence of false positives (i.e., cases in which a train is unnecessarily disallowed to proceed). The verification is carried out by exploiting the UMC model checking verification framework locally developed at ISTI-CNR.
2014
Lecture Notes in Computer Science Formal Methods for Industrial Critical Systems
19th International Conference on Formal Methods for Industrial Critical Systems
Florence; Italy
11-12 September 2014
Franco Mazzanti;Giorgio Oronzo Spagnolo;Simone Della Longa;Alessio Ferrari
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in FLORE sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificatore per citare o creare un link a questa risorsa: https://hdl.handle.net/2158/900142
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 15
  • ???jsp.display-item.citation.isi??? ND
social impact