原文传递
基于混成自动机的ZC子系统安全的验证方法研究
| 论文题名： | 基于混成自动机的ZC子系统安全的验证方法研究 |
| 关键词： | 城市轨道交通;列车控制系统;ZC子系统;混成自动机;行车安全 |
| 摘要： | 近年来，随着城市化进程的加速，城市轨道交通业已经成为市内交通的首选，用以缓解交通拥堵的情况。结合了通信技术，计算机技术与自动控制技术的基于通信的列车控制系统(Communication Based Train Control，CBTC)是我国使用的城市轨道交通控制系统。作为一个安全苛求系统和复杂系统，在完成系统设计开发之后验证系统性质是否符合设计需求和寻找安全隐患是一项重要的任务。现阶段对于系统安全的分析验证主要利用传统的故障树等经典安全分析方法以及基于形式化模型的系统安全验证。本文从CBTC系统混成特性角度，利用线性混成自动机模型对ZC子系统功能建模，验证ZC子系统是否满足设计需求及行车安全。 论文从CBTC系统原理及结构入手，总结出实时特性、安全特性、混合特性和并发特性四种CBTC系统具有的明显特征。目前对于实时与并发特性的研究有利用通信顺序进程与时间自动机形式化方法建立系统模型并进行验证。针对ZC子系统混成特性建模进行形式化验证的研究较少，混成特性关系到系统控制列车运行安全问题。本文提出利用线性混成自动机形式化方法对ZC子系统进行建模分析与性质验证。 文章选取扩展能力较强的统一建模语言(Unified Modeling Language，UML)对系统进行描述，利用元素构造型、标记值和约束的UML扩展方式对UML顺序图进行了时间与变量方面扩展，表现系统的实时、并发和混合特性。根据模型转换理论，将扩展后的UML顺序图转换为线性混成自动机。通过制定严格的转换规则，保证模型转换过程中的模型一致性问题。线性混成自动机作为自动机的一个分支，能够描述离散状态间连续变量的变化过程。 本文最后选取了ZC子系统中体现混成特性的列车跨越ZC边界越区切换控制功能，结合移动授权生成过程进行建模，并利用BACH混成自动机验证软件对模型性质与安全进行验证分析。证明了本文提出的ZC子系统安全验证方法的可行性与正确性。 |
| 作者： | 侯晓鹏 |
| 专业： | 交通信息工程及控制 |
| 导师： | 黄友能 |
| 授予学位： | 硕士 |
| 授予学位单位： | 北京交通大学 |
| 学位年度： | 2015 |
| 正文语种： | 中文 |
检索历史
应用推荐
