铁路车站计算机联锁软件建模研究

摘要

铁路车站计算机联锁系统是运用“故障-安全”技术、计算机技术、网络技术以及容错技术等实现进路控制功能的系统。它不仅是实时系统，而且是安全-苛求系统。铁路车站计算机联锁软件是一种安全苛求软件，它在保障站内的行车安全、行车作业效率的提升等方面都起到及其关键的作用，是铁路车站计算机联锁系统的关键组成。
　　目前，对联锁软件的设计阶段多采用自然语言，表现出很大的歧义性和二义性。本文基于面向对象理论，综合采用类图、用例图、协作图、序列图、状态图和活动图对联锁系统的进路控制过程及子过程进行建模。基于形式化方法，采用形式系统ALCQI-CTL，对模型进行形式化描述和说明，使模型的歧义性大大降低，减少主观因素差异造成的设计错误。
　　论文针对车站联锁软件建模进行研究:
　　(1)给出五元Kripke模型和语义，研究描述逻辑ALCQI，以及其语法和语义描述。基于形式系统ALCQI-CTL和形式系统ALCQI-CTL的序列图形式化方法，研究该系统的模型和形式化语义，并对该系统进行可行性分析。
　　(2)建立系统的静态模型，研究计算机联锁系统的软硬件的组成和功能，以基本联锁原理为基础，采用用例图对计算机联锁软件的组成和功能进行描述，并采用类图设计信号机、道岔、轨道区段和进路的数据描述以及采用状态图设计对象的状态变化模型。
　　(3)建立系统的动态模型，基于模块化思想，并且采用UML的一系列动态图建立一次进路控制过程的总体模型和过程的动态模型。建立一次进路控制过程和子过程的Kripke模型，基于形式系统ALCQI-CTL，并对其进行形式化描述和说明。
　　(4)对模型进行实验，完成相关功能的验证工作。
　　本文的研究结果表明:综合采用统一建模语言和形式化方法，能够高效地消除软件设计阶段由于人为因素差异造成的的缺陷和错误，使得计算机联锁领域专家和软件开发人员的联系更加紧密，提升联锁软件的安全性、可靠性;另一方面，能够在软件开发的初始阶段就及时发现软件设计中的缺陷和错误，同时，也减少了软件测试和验证的经济成本。验证结果表明:所建立的铁路车站计算机联锁软件的模型能充分应用于实际的需要。

目录

声明

摘要

1 绪论

1．1 研究背景

1．2 国内外研究动态

1．3 研究意义

1．4 主要研究内容及组织结构

2 理论研究

2．1 形式化方法

2．1．1 形式化方法发展历程

2．1．2 形式化方法综述

2．2 统一建模语言UML

2．2．1 UML综述

2．2．2 UML定义

2．3 描述逻辑与计算树逻辑

2．3．1 描述逻辑DL

2．3．2 描述逻辑ALCQI

2．3．3 计算树逻辑CTL

2．4 形式系统ALCQI-CTL

2．4．1 UML与描述逻辑的异同

2．4．3 基于形式系统ALCQI-CTL序列图的形式化

2．5 小结

3 静态模型的分析与设计

3．1 计算机联锁系统硬件结构

3．1．1 计算机联锁系统结构

3．1．2 计算机联锁系统工作原理

3．1．3 计算机联锁系统硬件组成

3．2 计算机联锁系统软件结构设计

3．2．1 计算机联锁系统软件总体设计

3．2．2 计算机联锁软件功能需求分析

3．3 计算机联锁系统静态模型设计

3．4 设备对象描述以及其状态变化

3．4．1 对象总体关系模型

3．4．2 信号机对象描述及其状态变化

3．4．3 道岔对象描述及其状态变化

3．4．4 轨道区段对象描述及其状态变化

3．4．5 进路对象描述

3．5 小结

4 动态模型的设计与形式化描述

4．1 进路控制过程

4．1．1 进路控制过程概述

4．1．2 进路控制过程分析

4．2 进路建立过程模型

4．2．1 进路选择过程模型

4．2．2 进路锁闭过程模型

4．2．3 信号开放过程模型

4．2．4 信号保持过程模型

4．2．5 进路建立过程模型

4．3 进路解锁过程模型

4．3．1 调车中途折返解锁过程模型

4．3．2 取消进路过程模型

4．3．3 人工解锁过程模型

4．4 一次进路控制过程总体模型

4．5 小结

5 模型的验证

5．1 联锁控制程序

5．1．1 总体设计

5．1．2 信息识别

5．1．3 操作界面

5．1．4 功能模块

5．2 仿真研究

5．3 小结

结论

致谢

参考文献

攻读学位期间的研究成果