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