Ten Diverse Formal Models for a CBTC Automatic Train Supervision System

TL;DR

This paper presents ten formal models for a CBTC train supervision system, demonstrating their application in a case study to analyze deadlock avoidance, and compares the modeling languages' features and impacts.

Contribution

Introduces ten diverse formal models for CBTC ATS systems and evaluates their differences and similarities through a comprehensive case study.

Findings

Models reveal commonalities and differences among formal verification languages.

Language characteristics significantly influence model formulation and analysis.

The case study demonstrates the practical application of multiple formal methods in train supervision.

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 considered, and we highlight the impact of the specific characteristics of each language on the presented models.