Ten Diverse Formal Models for a CBTC Automatic Train Supervision System
This work addresses deadlock prevention in metro train scheduling, but it is incremental as it applies an existing algorithm across multiple formal models without introducing new methods.
The authors tackled the problem of deadlock avoidance in Communications-based Train Control (CBTC) Automatic Train Supervision (ATS) systems by applying a deadlock avoidance algorithm in a case study, which they encoded using ten different formal verification environments to analyze commonalities and differences.
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 considered, and we highlight the impact of the specific characteristics of each language on the presented models.