铁路联锁系统的验证
软件工程
2015-06-12 v1 计算机科学中的逻辑
摘要
在铁路领域，联锁是一种计算机化系统，用于控制铁路信号对象以实现列车交通的安全运行。每个联锁使用称为应用数据的特定数据，该数据反映了受控车站的轨道布局。应用数据的验证与确认目前手动执行，因此容易出错且成本高昂。本文中，我们阐述了如何基于应用数据在NuSMV中构建铁路联锁的可执行模型。我们还详细介绍了为自动将应用数据转换为我们的模型而开发的工具。最后，我们展示了如何通过利用基于NuSMV的Python库PyNuSMV定制现有模型检测算法，在真实规模的车站模型上验证一组实际的安全属性。
引用
@article{arxiv.1506.03554,
title = {Verification of railway interlocking systems},
author = {Simon Busard and Quentin Cappart and Christophe Limbrée and Charles Pecheur and Pierre Schaus},
journal= {arXiv preprint arXiv:1506.03554},
year = {2015}
}
备注
In Proceedings ESSS 2015, arXiv:1506.03250