模型驱动的城轨列车车载控制系统软件评估体系

摘要

在城轨列车运行车载控制系统中，硬件和软件同等重要，车载硬件已经逐步采用标准工业计算机产品，而负责实现核心功能的软件，已经成为保障列车安全高效运营的一个重要因素。由软件错误导致事故发生将会造成生命财产重大损失，所以针对城轨车载软件开发前期过程中的模型建立，模型测试、模型验证方法的研究具有重要意义。列控系统软件是多层次结构的复杂系统，具有并发性、响应性特性和状态空间庞大的特点，研究适合描述软件需求的基于模型驱动的建模方法、模型状态的转换、相关测试序列生成验证方法和模型软件测试，全套流程已经成为城轨列控系统软件的系统级建模评估理论的研究重点。
　　根据城轨列控系统软件的需求及其实际功能相关的特点，提出了针对软件的建模技术、序列生成验证及测试方法。
　　建模方面，从城轨列控软件需求出发，提出了基于模型驱动的软件架构的需求分析和功能划分，以车载设备软件为应用对象，使用了标准化建模语言UML，以图形化方式表述软件系统过程和实现方法。分析了具体模型的分层架构，用两种静态图和两种动态图从不同层面对细节进行了描述，对内建关联进行了层次连接。
　　验证方面，介绍了模型检验的概念，说明了计算树逻辑(CTL)的扩展形式ASK-CTL在着色Petri网上的应用。从图的遍历角度，提出了深度优先算法在寻找有效测试路径的概念，并将算法运用于CPN Tools，以生成测试案例路径。引入实际的列控系统模型，提出了一种针对多线程的形式化定义ThrCPN及其图形描述，和基于对象UML模型的形式化建模方法ObjCPN。在层次化建模方法中，分别运用了ThrCPN和ObjCPN。提出了UML模型转换形式化有色Petri网的转换方法，缩小了功能模型到验证方案之间差距，简化了转换的复杂过程，形成了可验证的形式化模型。
　　测试序列生成方面，在CPN Tools工具中应用了ML编写的深度优先搜索算法，生成的测试序列，解决了并发系统不可达状态过多的问题。形式化验证方法生成的案例工具为形式化检验的主要于段。测试序列的生成对后期软件模拟测试起到了测试案例的作用。对证例路径的修改和完善，也为后期代码的标准化起到关键作用。
　　最后以城轨车载设备软件为测试对象，运用TestBed进行软件测试案例的生成和测试执行。比较了实际案例和形式化方法生成的路径，结果说明，基于模型驱动的软件建模方法可有效的实现系统的软件状态和行为，一定程度上约束了模型状态空间路径，且生成的针对软件需求的测试序列具有接近软件实际功能要求的特点。本方法还可用生成的模型指导应用软件的开发。

目录

声明

致谢

摘要

术语表

1．引言

1．1 研究背景

1．2 城轨信号系统的结构和特点

1．3 安全系统应用软件框架建模的内容和必要性

1．4 形式化建模研究现状

1．4．1 UML语言

1．4．2 Petri网

1．4．3 时间自动机

1．5 模型驱动软件开发(MDSD)的国内外研究现状

1．6 基于MDA的开发工具

1．7 选题的目的和意义

1．8 论文主要研究内容

1．9 篇章结构

2．模型驱动软件开发和软件质量评估的研究

2．1 模型驱动软件开发

2．1．1 MDSD发展背景

2．1．2 MDSD的概念

2．1．3 MDSD和MDA的区别

2．1．4 MDSD术语

2．1．5 软件体系结构

2．1．6 以体系结构为中心的设计

2．2 形式化方法

2．2．1 形式化方法与软件形式化

2．2．2 形式化方法与软件可靠性

2．2．3 面向对象软件形式化方法

2．3 软件评估

2．3．1 软件质量评估

2．3．2 软件可靠性评价

2．3．3 软件可靠性测试过程

2．4 软件评估体系的说明

2．5 本章小结

3．基于UML的模型定义及列控系统形式化建模

3．1 UML模型定义

3．1．1 UML语义及表示法

3．1．2 UML的分类及其模型图

3．1．3 类图的定义

3．1．4 状态图的定义

3．1．5 序列图的定义

3．2 UML模型建立

3．3 实例业务分析

3．3．1 ATO部分模块功能用例图

3．3．2 ATO部分模块功能类图

3．3．3 ATO部分模块功能状态图

3．3．4 ATO部分模块功能序列图

3．4 本章小结

4．Petri网建模与测试案例验证

4．1 Petri网的基本概念

4．1．1 基本Petri网

4．1．2 网的图形表示

4．1．3 网系统

4．1．4 Petri网的动态性质

4．1．5 Petri网工作流程基本结构

4．2 着色Petri网(CPN)定义

4．2．1 着色Petri网

4．2．2 CPN工具介绍

4．3 验证技术

4．3．1 模型检验

4．3．2 测试序列集生成算法

4．4 列车控制系统建模和验证实例

4．4．1 线程模型方法

4．4．2 对象模型方法

4．5 UML模型到Petri网模型的转换

4．5．1 UML类图到ObjCPN

4．5．2 UML状态图到ObjCPN

4．5．3 UML序列图到ThrCPN及ObjCPN

4．6 基于ObjCPN模型的层次化建模方法

4．6．1 被测系统模型

4．6．2 环境模型

4．6．3 系统模型

4．6．4 模型活性分析

4．7 测试序列生成算法

4．7．1 路径获取

4．7．2 测试序列生成

4．8 系统分析实例

4．8．1 共享内存管理模块分析

4．9 本章小结

5．模型测试

5．1 测试策略

5．1．1 软件检验的方法

5．1．2 软件测试工具介绍

5．1．3 代码验证标准

5．1．4 测试用例设计方法

5．1．5 测试环境

5．2 测试方案

5．2．1 测试规程

5．2．2 主要测试功能项

5．3 测试过程

5．3．1 模块结构分析

5．3．2 静态测试

5．3．3 动态测试

5．4 测试结果

5．4．1 串口模块测试结果

5．4．2 ZC接口模块的测试结果

5．4．3 共享内存模块测试结果

5．5 本章小结

6．研究结论与展望

6．1 研究结论

6．2 本文创新点

6．3 未来工作展望

参考文献

附录A 作者简历及科研成果清单

附录B 学位论文数据集