原文传递
基于SCADE的CBTC区域控制器软件开发
| 论文题名： | 基于SCADE的CBTC区域控制器软件开发 |
| 关键词： | 列车运行控制系统;SCADE模型;区域控制器;模型驱动开发;同步编程;LUSTRE语言;安全状态机 |
| 摘要： | 区域控制器(Zone Controller-ZC)是基于通信列车运行控制系统(Communications Based Train Control system-CBTC)系统的地面控制核心设备,负责列车移动授权的计算和运行安全保障。ZC是一个复杂庞大的安全关键系统,其软件开发在规范刻画、设计、验证等诸多方面面临挑战。近年来,基于模型的软件开发方法在安全关键领域逐渐被认可,本文研究基于SCADE模型的ZC软件开发方法,主要工作体现在如下方面: (1)以轨道交通控制系统为背景,研究了安全关键性系统的相关安全标准,分析了模型驱动开发的优势,并介绍了SCADE模型开发工具。 (2)研究了SCADE理论基础—同步编程理论。研究了LUSTRE语言的语法规则和UJSTRE语言对反应式系统的进行模型描述的抽象方法。分析了数据流图和安全状态机这两种形式化建模机制的语义基础、建模方法以及模型的特性。研究了同步编程理论对模型的两种确认方法模拟仿真和形式化验证。 (3)采用SCADE模型工具,对ZC进行建模。对ZC进行了形式化描述,建立ZC的SCADE总体模型。通过分析区域控制器控制列车的典型场景,将ZC的主要功能划分为列车管理功能、进路匹配功能和MA计算功能,详细的设计了各功能的软件流程。采用安全自动机建模机制,建立了列车管理功能的模型;采用数据流建模机制,建立了进路匹配功能和MA计算功能的模型。 (4)采用SCADE仿真与验证工具,对ZC模型进行检验。采用故障模式及影响分析方法,对ZC的主要功能进行了安全分析。使用SCADE模拟仿真模块,对模型进行了测试,使用SCADE形式化验证器,对模型的安全属性进行了验证,从而确认了模型的正确性。 通过对课题的研究,本文得出以下结论:基于SCADE模型的开发避免了对软件的重复性描述,避免了人工编写代码,能在系统设计初期发现设计缺陷,提高了软件质量和开发效率。 |
| 作者： | 张路 |
| 专业： | 交通信息工程及控制 |
| 导师： | 王海峰 |
| 授予学位： | 硕士 |
| 授予学位单位： | 北京交通大学 |
| 学位年度： | 2010 |
| 正文语种： | 中文 |
检索历史
应用推荐
