高速铁路列控系统形式化验证与Simulink/Stateflow仿真

中国高速铁路列控系统的形式化分析与验证是一篇发表在《中国科学:信息科学》(2015年第45卷第3期)的研究论文，由郭丹青、吕继东、王淑灵等人共同完成。高速铁路列控系统的安全性直接关系到乘客的生命财产安全，因此对其进行全面而严谨的形式化验证至关重要。然而，随着系统规模的扩大，软件和硬件的复杂性增加，直接进行形式化验证的难度日益增大。 文章提出了一种策略，即利用Simulink/Stateflow建模工具对列控系统的行车许可、等级升级以及部分模式转换进行图形化建模。这种模型具有高度的通用性，可以通过调整参数模拟多种等级转换和模式转换的组合场景。作者进行了10种不同组合情况的仿真，结果发现存在可能导致不正常停车或等级转换失败的问题。这表明，虽然仿真能有效地发现潜在问题，但它并不足以确保系统的绝对正确性，因为仿真本身存在不完备性，不能作为最终的验证手段。 鉴于此，文章强调了在安全关键系统设计中，形式化验证的必要性。针对发现的一个不正常停车的场景，作者进行了深入的形式化验证，旨在通过数学逻辑和自动化工具来确保系统的正确性和鲁棒性。这种结合仿真和形式化验证的方法，对于确保高速铁路列控系统的安全性具有实际价值，为提升整个系统的可靠性提供了新的思路和技术支持。同时，研究还得到了国家重点基础研究发展计划、国家高技术研究发展计划以及国家自然科学基金等多个项目的资助，体现了这一领域的研究重要性和跨学科的合作。