Database of Case Studies Achieved Using CADP

Formal Modeling and Verification of an Automatic Train Supervision System

Organisation: CNR-ISTI (ITALY)

Method: LNT
PROMELA
many others

Tools used: CADP (Construction and Analysis of Distributed Processes)
CPN Tools
FDR4
mCRL2
nuSMV
ProB
SPIN
TLA+
UMC
UPPAAL

Domain: Railways

Period: 2018

Size: up to 91,890,065 states and up to 453,321,793 transitions

Description: CBTC (Communication-Based Train Control) systems are a de-facto standard for metro networks. A principal component of a CBTC is the ATS (Automatic Train Supervision) system, which dispatches and monitors trains along the metro network according to a predefined set of missions. This case study concerns the modeling and verification of a scheduling algorithm, which shall avoid deadlock situations while ensuring that all missions are completed, regardless of train delays.

This case study applies ten different formal methods to the same algorithm, to increase the confidence in its correctness and to compare the merits of the various formal methods. Therefore, all models share the same basic modeling scheme (called a "basic blackboard model"), encoded in various ways depending on the modeling languages, rather than dedicated models optimized to fit in the best possible way to each formalism. All models are archived in the model repository of the MARS workshop series: http://mars-workshop.org/repository.html

Conclusions: Among the advantages of CADP, the authors note the imperative modeling style of LNT fitting their state-machine oriented representation, the expressive power of the property definition language MCL (that subsumes both LTL and CTL), and the fact that "the verification tools can be used in their default configuration without having to specify any particular evaluation choice."

Concerning performance, CADP is among both the fastest tool and among those with the lowest memory requirements.

Publications: [Mazzanti-Ferrari-18] Franco Mazzanti and Alessio Ferrari. "Ten Diverse Formal Models for a CBTC Automatic Train Supervision System". Proceedings of the 3rd Workshop on Models for Formal Analysis of Real Systems (MARS'18), Thessaloniki, Greece, EPTCS 268, pages 104-149, April 2018.
Available on-line at: https://arxiv.org/pdf/1803.10324.pdf
or from our FTP site in PDF or PostScript

[Mazzanti-Ferrari-Spagnolo-18] Franco Mazzanti, Alessio Ferrari, and Giorgio O. Spagnolo. "Towards Formal Methods Diversity in Railways: An Experience Report with seven Frameworks". Software Tools for Technology Transfer 20(3), pages 263-288, June 2018.
Available on-line at: https://link.springer.com/article/10.1007/s10009-018-0488-3
or from our FTP site in PDF or PostScript

Contact:
Franco Mazzanti
Istituto di Scienza e Tecnologie dell'Informazione "A. Faedo"
Area della Ricerca CNR di Pisa
Via G. Moruzzi, 1
56124 - Pisa
Tel: +39 (0)50 315 2919
Fax: +39 (0)50 315 2810
E-mail: franco.mazzanti at isti.cnr.it



Further remarks: This case-study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies


Last modified: Mon Feb 11 12:56:58 2019.


Back to the CADP case studies page