基于SCADE的CBTC区域控制器建模与验证

摘要

随着城市化进程的推进和城市人口的增加，人们越来越意识到城市轨道交通的优点，全国各地也在大力兴建城市轨道交通。基于通信的列车运行控制系统(Communication-based Train Control，CBTC)具有安全、高效等优点，是现代城市轨道交通列车运行控制系统今后的发展方向。
　　区域控制器(Zone Controller，ZC)是CBTC系统的核心地面设备，它的主要功能是为控制范围的列车计算并分配移动授权（Movement Authority，MA）保证列车在线路上的运行安全。ZC是安全苛求系统，必须符合SIL-4级的安全等级需求，因此在对ZC系统设计和开发时，要用最为安全性高的方法。高安全性应用开发环境SCADE运用基于模型的方式为安全苛求系统提供完整的解决方案，用它来开发ZC这种高安全性的软件是十分合适的。
　　本文采用SCADE对ZC建模，主要是对ZC的主要功能——列车管理功能和MA计算功能进行模型的建立。列车管理功能的核心是对列车状态的管理，不管列车处于何种运行状态，ZC都必须有效的对列车进行管理。MA计算是ZC的核心功能，ZC实时的与CBTC的其他子系统通信，为控制范围的列车计算MA，确保列车的运行安全。对于列车管理功能，采用SCADE的安全状态机来进行模型的建立;对于MA计算功能，采用SCADE的数据流图来进行模型的建立。
　　最后，利用SCADE的仿真和验证工具对建立的列车管理模型和MA计算模型进行验证。对模型进行了仿真测试，保证了系统的正确性。对模型进行覆盖率分析，确保了仿真测试的完备性。使用SCADE的形式化验证功能对系统的安全属性进行验证，证明了模型的安全性。

目录

声明

摘要

第1章 绪论

1．1 研究背景与意义

1．2 国内外研究现状

1．2．1 CBTC系统的发展现状

1．2．2 SCADE应用情况

1．3 CBTC系统及ZC简介

1．3．1 CBTC系统结构及原理

1．3．2 ZC概述

1．4 论文的主要内容

第2章 SCADE及其功能介绍

2．1 SCADE产生背景

2．2 SCADE功能模块介绍

2．3 SCADE图形化建模

2．3．1 数据流图模型

2．3．2 安全状态机模型题

2．4 SCADE模型的验证

2．4．1 模型仿真验证

2．4．2 形式化验证

2．5 本章小结

第3章 基于SCADE的ZC系统功能建模

3．1 移动闭塞原理

3．2 列车管理功能建模

3．2．1 列车运行状态分析

3．2．2 列车管理功能SCADE模型

3．3 MA计算功能建模

3．3．1 移动授权计算原理

3．3．2 移动授权计算的障碍物分析

3．3．3 不同场景下移动授权计算

3．3．4 MA计算功能SCADE模型

3．4 本章小结

第4章 ZC功能模型的验证

4．1 SCADE验证方法

4．2 模型仿真

4．2．1 列车管理模型仿真

4．2．2 MA计算模型仿真

4．3 模型覆盖率分析

4．4 模型的形式化验证

4．5 本章小结

结论与展望

结论

展望

致谢

参考文献

攻读硕士学位期间发表的论文及科研成果