基于UML-NuSMV模型的列控系统需求阶段的安全分析

摘要

在中国的交通运输体系中，铁路已经成为其中最重要的基础设施和最大众化的交通工具。而列车运行控制系统（简称列控系统）是保证列车行车安全和高效运行的关键装备，是整个铁路系统的核心技术。一旦列控系统出现安全性问题，极有可能导致行车中断，甚至是车毁人亡的灾难。因此，在列控系统开发的早期，即需求阶段对系统进行安全分析尤为重要。
　　列控系统的研究采用国际通用的方法——“标准先行”，即先完成系统规范的制定，然后以此指导后续的系统开发。故此，本文对于列控系统需求阶段的安全分析是以列控系统需求规范作为研究对象，并对其描述的系统进行建模分析与形式化验证，然后建立故障模型进行融合完成安全分析。主要的研究内容如下:
　　1、采用统一建模语言(Unified Modeling Language，UML)对列控规范进行初期建模分析，从系统需求、静态结构和动态行为三个维度抽象出列控系统的主要特征，并对建模语言进行了扩展设计，增强建模语言的刻画能力。
　　2、运用转换规则，将UML模型转换成形式化NuSMV模型，利用形式化技术完成需求规范的验证，奠定后续安全分析的基础。提出故障模式的失效符号标记，产生融合故障模型的形式化模型，完成本文提出的基于UML-NuSMV模型的列控系统需求阶段安全分析的工作。
　　3、为列控系统需求阶段的属性验证和安全分析开发了支持工具:RMTool。该工具实质是一个插件，集成到（Rational Software Architect，RSA）平台，通过相关的接口与形式化工具、UML模型进行链接，实现模型转换、属性验证以及安全分析三大主要功能，较好地辅助本文研究内容的展开。

目录

声明

致谢

摘要

1 引言

1．1 研究背景

1．1．1 问题的提出

1．1．2 列控系统需求工程发展现状

1．2 国内外研究现状

1．2．1 列控系统需求研究现状与常见安全分析方法

1．2．2 需求工程相关的安全分析工具集成平台研究现状

1．2．3 研究现状的总结与分析

1．3 论文的主要工作及组织架构

1．4 本章小结

2 列控系统需求规范与基于故障注入模型的安全分析方法

2．1 CTCS-3级列控系统规范介绍

2．2 列控系统需求规范的特点

2．3 基于故障注入模型的安全分析在需求阶段的分析过程

2．3．1 相关的术语和概念

2．3．2 系统安全评估过程

2．3．3 基于故障注入模型的安全分析过程

2．3．4 基于UML-NuSMV模型的安全分析过程

2．4 本章小结

3 UML模型的设计与列控系统需求规范建模

3．1 UML系统建模语言

3．1．1 UML概述

3．1．2 UML扩展机制

3．1．3 RSA建模工具

3．2 基于UML的CTCS-3级列控系统需求规范建模

3．2．1 系统需求分析

3．2．2 静态结构分析

3．2．3 动态行为分析

3．3 本章小结

4 NuSMV的研究与列控系统需求阶段的安全分析

4．1 NuSMV形式化模型的研究

4．1．1 NuSMV语言的介绍

4．1．2 UML模型到NuSMV模型的转化

4．2 故障模型的形式化研究

4．2．1 故障模式的失效描述符号

4．2．2 故障模型标记语言的定义

4．2．3 故障模型与NuSMV模型的融合

4．3 列控系统需求阶段的安全分析

4．3．1 逻辑计算公式的介绍

4．3．2 需求阶段的安全分析过程

4．4 本章小结

5 UML-NuSMV模型分析工具RMTool的开发

5．1 基于UML-NuSMV模型的系统需求阶段安全分析体系结构

5．2 RMTool开发运行环境的约束

5．2．1 软件约束

5．2．2 硬件约束

5．3 RMTool工具的界面设计及功能实现

5．3．1 RMTool工具的界面设计

5．3．2 视图扩展

5．3．3 模型验证操作

5．3．4 安全分析操作

5．4 本章小结

6 案例分析

6．1 案例背景介绍

6．2 RBC切换场景的需求建模与安全分析

6．2．1 RBC切换场景介绍及假设

6．2．2 RBC切换场景建模与需求规范验证

6．2．3 RBC切换场景的安全分析

6．3 本章小结

7 总结与展望

参考文献

表目录

图目录

作者简历

学位论文数据集