CBTC Automatic Train Supervision System
| Description: | Ten models for a CBTC automatic train supervision system |
| Author(s): | Franco Mazzanti, Alessio Ferrari |
| Event(s): | MARS'18 |
| Paper(s): |
Ten Diverse Formal Models for a CBTC Automatic Train Supervision System |
Abstract
Communications-based Train Control (CBTC) systems are metro signalling platforms, which coordinate and protect the movements of trains within the tracks of a station, and between different stations. In CBTC platforms, a prominent role is played by the Automatic Train Supervision (ATS) system, which automatically dispatches and routes trains within the metro network. Among the various functions, an ATS needs to avoid deadlock situations, i.e., cases in which a group of trains block each other. In the context of a technology transfer study, we designed an algorithm for deadlock avoidance in train scheduling. In this paper, we present a case study in which the algorithm has been applied. The case study has been encoded using ten different formal verification environments, namely UMC, SPIN, NuSMV/nuXmv, mCRL2, CPN Tools, FDR4, CADP, TLA+, UPPAAL and ProB. Based on our experience, we observe commonalities and differences among the modelling languages consid- ered, and we highlight the impact of the specific characteristics of each language on the presented models.
Model(s)
-
- Download Model
- Browse Model
- tool(s): UMC
-
- Download Model
- Browse Model
- tool(s): Promela (Spin)
-
- Download Model
- Browse Model
- tool(s): NuSMV/nuXmv
-
- Download Model
- Browse Model
- tool(s): mCRL2
-
- Download Model
- Browse Model
- tool(s): CPN tools
-
- Download Model
- Browse Model
- tool(s): FDR4
-
- Download Model
- Browse Model
- tool(s): LNT (CADP)
-
- Download Model
- Browse Model
- tool(s): TLA toolbox
-
- Download Model
- Browse Model
- tool(s): Uppaal
-
- Download Model
- Browse Model
- tool(s): ProB
This work is licensed under a Creative Commons
Attribution-NonCommercial-ShareAlike 4.0 International License.