CBTC 自动列车监督系统的十种多样化形式化模型
软件工程
2018-03-29 v1 形式语言与自动机理论
计算机科学中的逻辑
系统与控制
摘要
基于通信的列车控制（CBTC）系统是地铁信号平台，用于协调和保护车站轨道内以及不同车站之间列车的运行。在 CBTC 平台中，自动列车监督（ATS）系统发挥着重要作用，它在地铁网络内自动调度和安排列车路线。在各项功能中，ATS 需要避免死锁情况，即一组列车互相阻塞的情况。在一项技术转移研究的背景下，我们设计了一种用于列车调度的死锁避免算法。在本文中，我们介绍了一个应用该算法的案例研究。该案例研究使用十种不同的形式化验证环境进行编码，即 UMC、SPIN、NuSMV/nuXmv、mCRL2、CPN Tools、FDR4、CADP、TLA+、UPPAAL 和 ProB。基于我们的经验，我们观察了所考虑的建模语言之间的共性与差异，并强调了每种语言的特定特征对所提出模型的影响。
引用
@article{arxiv.1803.10324,
title = {Ten Diverse Formal Models for a CBTC Automatic Train Supervision System},
author = {Franco Mazzanti and Alessio Ferrari},
journal= {arXiv preprint arXiv:1803.10324},
year = {2018}
}
备注
In Proceedings MARS/VPT 2018, arXiv:1803.08668