文档介绍：中文摘要
中文摘要
摘要在现代公共交通体系中,轨道交通系统具有不可替代的突出地位。目前,
我国的轨道交通正处在一个史无前例的大发展时期,人们对它有着很高的期望和
要求。如何实现列车安全、快速、高效地运行,是摆在相关科研人员面前的一个
突出问题。列车运行控制系统作为轨道交通系统的神经中枢,担当着保障行车安
全和提高列车运行效率的重任。随着计算机技术在列车运行控制系统中的应用,
安全问题显得越发的重要和复杂,传统的安全系统设计、分析和测试方法难以满
足以计算机技术为基础的安全系统的需要。近年来,基于离散数学和形式逻辑理
论的形式化方法发展迅速,为解决安全计算机系统设计开发的正确性问题提供了
一条可能的途径。
论文针对轨道交通列车运行控制系统的特点,研究安全系统设计的理论和方
法,尝试采用形式化方法进行系统安全设计和验证。论文主要以列车运行控制系
统为研究对象,选择自动机模型和模型检验方法分别作为系统形式化建模和验证
的方法,提出时间自动机网络模型和相应的模型检验算法,进而给出形式化设计
验证方法砚司
,最后以大连快轨号线车载设备为对象进行相关设计和验证,取
得了不错的效果。这些成果这对于提高国内轨道交通列车运行控制系统的安全性
设计水平,掌握系统关键技术,推动列车运行控制系统国产化具有重要的理论价
值和实践意义。
论文主要的创新点有以下几个方面
针对轨道交通列车运行控制系统的特点,在有限自动机模型的基础上提出
时间自动机网络模型,并且给出模型的形式化定义和相关特性,提出时间自动机
网络模型的形式化描述语言语言。和经典自动机模型相比,时间自动机网络
模型有以下优点①通过时间自动机网络模型,部分解决了经典自动机状态复杂
性问题,使得建模过程变得较为简便,有助于进行系统的形式化设计和验证②
通过在组件自动机内部和组件自动机之间加入时间约束集,可以对系统的实时性
进行描述③通过描述组件自动机之间的动作集,可以描述系统的并发行为④
通过连续变量区域化方法有效的压缩了系统的状态数,解决了经典自动机理论不
能描述连续变量的缺陷。
提出时间自动机网络模型的模型检验方法和步骤,主要的创新之处在于
①提出组件自动机一种时间自动机转换为带有时钟状态的有限自动机进行模
型检验的思想②基于数据结构,提出计算时钟状态和状态迁移时间约束的
北京交通大学博士学位论文
算法③提出公式在结构上进行模型检验的算法,可以对系统安全
性、无死锁性和系统响应实时性进行验证。
提出形式化设计验证方法’垅
在需求捕捉阶段采用时间自动机网络模型描述
系统需求在系统设计阶段,采用模型检验方法证明设计和需求的一致性,并保
证系统设计满足系统的安全性要求在系统开发阶段,从系统需求的形式化模型
开始逐步求精,得到层次化、模块化的系统实现框架。基于时间自动机网络的形
式化设计验证方法。日人有以下特点①通过设计时间自动机网络中组件自动机
之间的时间约束来满足系统实时性的要求,采用顺序图和模型验证方法可以
描述和验证系统的时间特性②通过采用方法作为形式化开发的方法,对于系
统的时间自动机网络模型进行不断精化,反复迭代,可以获得进行系统开发的伪
代码,保证系统开发和规范的一致性。
论文最后以大连快轨号线车载设备为应用对象,采用’方法完
成了车载设备控制系统的设计,采用时间自动机网络模型作为形式化描述语
言,对于系统的相关特性进行分析和模型验证。通过方法可以及时发现系
统设计错误和缺陷在多任务调度模型设计中,当设计模型不能满足系统的实时
性要求时,叮’方法会给出反例,指出错误发生的场景,直到设计模型满足实
时性要求为止。
关键词轨道交通列车运行控制系统形式化方法时间自动机网络
模型检验。
二。盯, 川
,
仙,阴
】哪
邵出
加凶明,
斤
苏
,
·
七
山“而做比
曰,
如比,
云别一门’恤、乞
朗旧
、,
,翻
仃叨
朋例
下目训
的阴出
。①
,胡
印尽②
助③
似④几。丘沈加以
翻如
北京交通大学博士学位论文
幻刀记
砂而①耐小
②
, 币
③肠即“肠卯
丫
认、乞
,
二】
比,吸
找论七右勿,助
山下丘即孔祖’①
记竹翻
②
曲
。几
,门’比即
人”界记明
勿,
一一
,’
致谢
本文是在唐涛教授的亲切关怀和具体指导下独立完成的。在攻读博士学位的
整个过程中,唐涛教授严谨的治学精神、对于学科前沿发展动向敏锐