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 the CADP Web 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 the CADP Web 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

Back to the CADP case studies page