轨道交通列车运行控制系统的形式化建模和模型检验方法研究

摘要

在现代公共交通体系中，轨道交通系统具有不可替代的突出地位。目前，我国的轨道交通正处在一个史无前例的大发展时期，人们对它有着很高的期望和要求。如何实现列车安全、快速、高效地运行，是摆在相关科研人员面前的一个突出问题。列车运行控制系统作为轨道交通系统的神经中枢，担当着保障行车安全和提高列车运行效率的重任。随着计算机技术在列车运行控制系统中的应用，安全问题显得越发的重要和复杂，传统的安全系统设计、分析和测试方法难以满足以计算机技术为基础的安全系统的需要。近年来，基于离散数学和形式逻辑理论的形式化方法发展迅速，为解决安全计算机系统设计开发的正确性问题提供了一条可能的途径。 论文针对轨道交通列车运行控制系统的特点，研究安全系统设计的理论和方法，尝试采用形式化方法进行系统安全设计和验证。论文主要以列车运行控制系统为研究对象，选择自动机模型和模型检验方法分别作为系统形式化建模和验证的方法，提出时间自动机网络模型和相应的模型检验算法，进而给出形式化设计验证方法ForTAN(FormalDesignandVerificationMethodsbasedonTimedAutomataNetwork)，最后以大连快轨3号线ATP车载设备为对象进行相关设计和验证，取得了不错的效果。这些成果这对于提高国内轨道交通列车运行控制系统的安全性设计水平，掌握系统关键技术，推动列车运行控制系统国产化具有重要的理论价值和实践意义。 论文主要的创新点有以下几个方面： (1)针对轨道交通列车运行控制系统的特点，在有限自动机模型的基础上提出时间自动机网络模型，并且给出模型的形式化定义和相关特性，提出时间自动机网络模型的形式化描述语言TAN语言。和经典自动机模型相比，时间自动机网络模型有以下优点：①通过时间自动机网络模型，部分解决了经典自动机状态复杂性问题，使得建模过程变得较为简便，有助于进行系统的形式化设计和验证；②通过在组件自动机内部和组件自动机之间加入时间约束集，可以对系统的实时性进行描述；③通过描述组件自动机之间的动作集，可以描述系统的并发行为；④通过连续变量区域化方法有效的压缩了系统的状态数，解决了经典自动机理论不能描述连续变量的缺陷。 (2)提出时间自动机网络模型的模型检验方法和步骤，主要的创新之处在于： ①提出组件自动机(一种时间自动机)转换为带有时钟状态的有限自动机进行模型检验的思想；②基于DBM数据结构，提出计算时钟状态和状态迁移时间约束的算法；③提出TCTL公式在Kripke结构上进行模型检验的算法，可以对系统安全性、无死锁性和系统响应实时性进行验证。 (3)提出形式化设计验证方法ForTAN(FormalDesignandVerificationMethodsbasedonTimedAutomataNetwork)：在需求捕捉阶段采用时间自动机网络模型描述系统需求；在系统设计阶段，采用模型检验方法证明设计和需求的一致性，并保证系统设计满足系统的安全性要求；在系统开发阶段，从系统需求的形式化模型开始逐步求精，得到层次化、模块化的系统实现框架。基于时间自动机网络的形式化设计验证方法ForTAN有以下特点：①通过设计时间自动机网络中组件自动机之间的时间约束来满足系统实时性的要求，采用UML顺序图和模型验证方法可以描述和验证系统的时间特性；②通过采用B方法作为形式化开发的方法，对于系统的时间自动机网络模型进行不断精化，反复迭代，可以获得进行系统开发的伪代码，保证系统开发和规范的一致性。 论文最后以大连快轨3号线ATP车载设备为应用对象，采用ForTAN方法完成了ATP车载设备控制系统的设计，采用时间自动机网络模型作为形式化描述语言，对于系统的相关特性进行分析和模型验证。通过ForTAN方法可以及时发现系统设计错误和缺陷：在多任务调度模型设计中，当设计模型不能满足系统的实时性要求时，ForTAN方法会给出反例，指出错误发生的场景，直到设计模型满足实时性要求为止。

目录

文摘

英文文摘

致谢

第一章绪论

1.1选题的背景

1.2列车运行控制系统安全技术的演变和发展

1.2.1列车运行控制系统发展初期和故障—安全概念的产生

1.2.2列车运行控制系统的电气化和故障安全技术的发展

1.2.3计算机时代的列车运行控制系统和安全性技术的应用

1.2.4列车运行控制系统安全性设计遇到的挑战

1.3形式化方法的发展和应用情况

1.4选题的目的和意义

1.5论文的主要研究工作和篇章结构

第二章形式化建模和模型检验方法

2.1形式化建模和验证方法的选择

2.1.1形式化建模方法的选择

2.1.2形式化验证方法的选择

2.2基于自动机理论的模型检验方法

2.2.1 Partial order技术

2.2.2 On-the-fly技术

2.2.3二叉判定图和符号模型检验

2.3模型检验的优化技术

2.4实时系统模型检验方法

2.4.1离散实时系统模型检验

2.4.2连续实时系统模型检验

2.5本章小结

第三章时间自动机网络模型及其模型检验方法研究

3.1经典自动机模型的局限性

3.2时间自动机网络模型

3.2.1时间自动机网络模型的形式化定义

3.2.2时间自动机网络模型的形式化描述语言

3.3基于时间自动机网络的模型检验方法

3.3.1组件自动机转换为带有时钟状态的有限自动机

3.3.2组件自动机的同步积复合

3.3.3时间自动机网络转换为Kripke结构

3.3.4用TCTL公式表示所要验证的系统属性

3.3.5模型检验算法

3.4本章小结

第四章形式化设计验证方法研究

4.1形式化设计建模

4.2形式化验证

4.3形式化开发

4.4本章小结

第五章大连快轨3号线ATP车载设备的形式化设计与验证

5.1系统需求

5.2 ATP车载设备需求分析

5.3系统功能

5.4形式化设计和验证

5.4.1需求分析

5.4.2形式化建模和设计

5.4.3形式化验证

5.4.4形式化开发

5.5本章小结

第六章结论

6.1论文总结

6.2展望

参考文献

附录A ATP车载控制系统实时性模型描述程序

作者简历

博士研究生期间发表论文目录

学位论文版权使用授权书及独创性声明