基于模型驱动的计算机联锁软件开发方法的研究与实现

摘要

计算机联锁系统(CBI)是铁路运输中的重要设备,它肩负着列车调度、安全行车、提高运输效率的重要工作。它通过对道岔、进路以及信号的控制,来实现铁路列车的调度指挥工作。随着计算机技术在铁路信号中的发展与应用,传统的分析设计方法已经无法满足当前社会对于铁路运输的安全性、高效性需求。为此我们采用模型驱动的嵌入式软件开发方法对联锁软件的设计与验证提出了新的思路,从而提高软件开发的精确性和高效性。
　　本文首先深入研究了各种形式化建模语言在嵌入式软件中的应用,以及它们在当前国际国内的发展水平和未来发展趋势。主要对各个方法的优点与缺点进行了对比分析,找出了一种适合计算机联锁系统软件开发的以模型设计需求分析取代传统文本设计需求分析的方法,即时间自动机理论。
　　本文以工大高科自主研发的计算机联锁系统软件GKI-33e为研究对象,对它的进路办理流程进行了深入的分析,根据EN系列标准以及国家铁路标准对它的安全性和功能性进行了主要描述,提出了软件设计的V模型。并根据此设计流程对进路办理流程进行了形式化建模与分析。
　　本文针对进路办理中的五个主要阶段分别建立了对应的时间自动机模型,并且通过成熟的UPPAAL工具组建了时间自动机网络,并对该网络进行了仿真模拟,通过时间约束与全局变量的设定,解决了以往开发过程中存在的模糊性、二义性等问题。
　　最后,本文从系统的功能性与安全性出发,对时间自动机网络进行了验证。通过BNF语法对系统安全功能进行了验证与分析。证明了以模型驱动方法为基础的嵌入式软件开发方法的可行性。为计算机联锁系统软件设计提供了重要的参考价值。

目录

封面

声明

致谢

中文摘要

英文摘要

目录

插图清单

表格清单

1 引言

1.1选题背景

1.2国内外研究现状

1.3课题来源

1.4本文的主要工作与结构

2建模语言的研究现状

2.1模型驱动的描述方法

2.2 联锁系统软件建模方法

2.3基于联锁软件的各建模方法的优缺点

2.4研究现状总结与分析

2.5本章小结

3 软件系统设计与需求分析

3.1 GKI-33e计算机联锁系统软件设计开发流程

3.2系统逻辑架构

3.3 系统需求分析

4 进路办理流程与基于时间自动机理论的建模

4.1 GKI-33e计算机联锁软件进路办理流程的分析

4.2进路控制流程中各个阶段的建模

4.3 进路办理各阶段模型建立

4.4 本章小结

5 基于UPPAAL的进路控制流程的验证与分析

5.1时间自动机网络

5.2 时间自动机网络的模拟

5.3进路各阶段的仿真模拟

5.4验证

5.5本章小结

6 结论与展望

6.1论文总结

6.2 展望

参考文献

攻读硕士学位期间的学术活动及成果情况