详情

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

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