作者：曹源; 唐涛; 徐田华; 穆建成交通信息工程形式化方法列车运行控制系统安全苛求系统
摘要：为了确保列车运行控制系统设计和开发的正确性，比较了仿真、测试和形式化3种能够验证系统设计正确性的方式。根据列车运行控制系统对安全的苛求性，提出了4个与系统安全相关的重要特性，即实时性、混成性、分布（并发）性、反应性，并分析了与这些特性相关的具体形式化方法。通过对每种形式化方法的数学基础和应用范围的分析和归类，给出了各种方法的优势和不足。分析结果表明：任何形式化方法的应用都具有一定的局限性，这是由模型检验和定理证明的本质所决定的；指出了新方法提出、既有方法拓展以及多方法集成将是列车运行控制系统的形式化领域的方向。
注：因版权方要求，不能公开全文，如需全文，请咨询杂志社
