基于SCADE的计算机联锁系统建模与验证

摘要

计算机联锁系统是铁路信号系统中保证行车安全的重要设备，失效后可能导致重大人员伤亡和财产损失，系统功能逻辑需要具备很高的安全性要求。然而，传统的计算机联锁系统主要采用手工编码的方式进行开发，软件质量主要依赖于代码评审、走查、测试等人工方式进行保障，存在一定的主观性，无法满足计算机联锁系统的高安全性要求。
　　形式化建模是安全关键系统开发的重要方法之一，具有严格的数学基础，能够准确和无歧义地描述系统需求，并且实现逻辑推理，能够有效地解决传统软件开发方法中存在的模糊性和二义性等问题。SCADE是基于形式化建模方法的高安全性软件开发环境，其提供安全状态机和数据流图两种形式化建模方法，能够直观、清晰、全面地描述软件功能逻辑;结合模型仿真和形式化验证能够直观、全面地分析模型的正确性和安全性，避免软件开发人员的主观性;最后自动生成面向工程的高质量的C代码。
　　本文研究基于SCADE的计算机联锁软件开发方法，利用SCADE的需求管理、形式化建模、模型仿真、形式化验证等工具来保证计算机联锁软件的正确性和安全性，具体包括以下内容:
　　(1)介绍了SCADE的软件开发模式和同步假设理论，并详细分析了SCADE的需求管理、安全状态机和数据流图建模、模型仿真、形式化验证以及代码生成机制。
　　(2)分析了计算机联锁系统的基本结构、特点及软件功能，根据系统需求将计算机联锁进路控制过程划分为进路选择、进路锁闭、信号开放、信号保持开放、正常通过进路解锁、取消进路六个阶段，分析各阶段中计算机联锁系统SCADE建模的具体需求。
　　(3)采用安全状态机和数据流图两种建模方法，建立计算机联锁系统进路控制过程的形式化模型。
　　(4)利用SCADE需求管理工具分析计算机联锁系统需求、概要设计和形式化模型之间的追溯关系，保证SCADE模型完全覆盖计算机联锁系统的系统需求和概要设计需求。
　　(5)通过图形化的模型仿真，保证计算机联锁软件模型的正确性;然后提取系统安全属性，利用形式化验证检测计算机联锁模型满足预期的安全属性;最后利用代码生成器自动生成面向工程的C代码。

目录

声明

摘要

1．1 研究背景及意义

1．2 国内外研究现状

1．2．1 联锁国内外发展现状

1．2．2 形式化方法在计算机联锁系统中的研究现状

1．3 论文主要内容及结构

第2章 高安全性应用开发环境

2．1 SCADE概述

2．2 SCADE软件开发模式

2．2．1 传统“V”型软件开发模式

2．2．2 SCADE“Y”型软件开发模式

2．3 SCADE Suite功能详解

2．3．1 需求管理

2．3．2 模型仿真

2．3．3 形式化验证

2．3．4 代码生成模块

2．4 SCADE建模机制

2．4．1 同步假设

2．4．2 数据流图

2．4．3 安全状态机

第3章 计算机联锁系统逻辑

3．1 计算机联锁系统概述

3．2 计算机联锁系统的特点

3．3 计算机联锁系统软件功能

3．3．1 进路建立子系统

3．3．2 进路解锁子系统

第4章 基于SCADE的计算机联锁系统建模

4．1 计算机联锁系统需求管理

4．2 计算机联锁系统建模

4．2．1 计算机联锁系统集层模型

4．2．2 进路选择模块

4．2．3 进路锁闭模块

4．2．4 信号开放模块

4．2．5 信号开放保持模块

4．2．6 正常通过解锁模块

4．2．7 取消进路模块

第5章 基于SCADE的计算机联锁模型验证

5．1 计算机联锁系统模型覆盖率分析

5．2 计算机联锁系统仿真分析

5．3 计算机联锁系统形式化验证

5．4 计算机联锁软件代码生成

结论

致谢

参考文献

附录