原文传递
CBTC中轨旁安全计算机的设计与形式化验证
| 论文题名： | CBTC中轨旁安全计算机的设计与形式化验证 |
| 关键词： | CBTC;轨旁安全计算机;列车控制 |
| 摘要： | 随着计算机越来越多的应用于安全苛求系统中，计算机能否长期安全、可靠、稳定的运行成为人们关注的中心，这促使着越来越多的人开始研究和设计安全计算机。而系统的安全性必须在设计阶段充分考虑，以免由于设计的缺陷导致整个系统存在安全隐患。所以在系统的设计过程中，根据安全苛求系统的“V"型的开发框架，采用形式化的方法对系统的安全性进行建模分析，验证系统设计的正确性和完备性是必要的。 论文以基于通信的列车控制(CBTC)系统中ZC应用和DSU应用作为应用背景，以CBTC系统中ZC应用和DS应用所使用的安全计算机平台为例。详细分析了安全计算机平台需求，在此基础上确定了系统结构，然后设计其硬件结构和软件的调度策略。 论文引入有色Petri网，根据安全性设计思想，在系统的设计阶段对安全计算机平台进行形式化建模。首先介绍了有色Petri网的形式化层次化建模的方法，然后根据系统结构，采用“自上而下"的层次建模方法对系统建立的顶层模型和各级子模型，子模型包括“主”“备”通道模型、通道内单机模型、容错和安全管理单元(FTSM)模型和通信控制器模型。 在所建模型的基础上，研究了CPN的状态空间分析和仿真性能分析两种方法在模型分析的应用。利用状态空间分析验证了容错和安全管理单元(FTSM)模块的有界性、活性等动态行为属性和逻辑功能的正确性；利用仿真分析完成了系统同步过程的性能分析，得出系统同步的时间参数，对系统调度时间的选取具有指导意义。通过对安全计算机进行建模和分析，可以验证对我们系统设计是否合理，对系统设计的完善提供参考和指导。 |
| 作者： | 袁彬彬 |
| 专业： | 交通信息工程及控制 |
| 导师： | 唐涛 |
| 授予学位： | 硕士 |
| 授予学位单位： | 北京交通大学 |
| 学位年度： | 2008 |
| 正文语种： | 中文 |
检索历史
应用推荐
