原文传递
EVENT-B方法在铁路车站连锁规范形式化建模与验证中的应用研究
| 论文题名： | EVENT-B方法在铁路车站连锁规范形式化建模与验证中的应用研究 |
| 关键词： | 铁路车站;联锁系统;形式化描述;EVENT-B方法;可视化仿真 |
| 摘要： | 安全苛求型系统指对安全性和可靠性有特殊要求的系统。铁路车站的联锁系统是一种典型的安全苛求型系统，其作用是组织列车和调车在铁路车站内行车，同时保证其行车安全和行车效率，因此使用有效的方法尽可能地保证联锁系统功能的安全性和可靠性显得非常有必要。通过对软件系统和硬件系统的需求规范进行形式化描述，建立模型并验证，可完善系统设计需求，从而提高系统开发过程的可靠性。 论文以铁路车站的联锁系统为研究对象，对其选排进路、锁闭进路、信号开放、信号保持、解锁进路的控制流程进行了详细的分析，并提取出了联锁系统较为关键的一些环境类规范和技术规范，同时基于EVENT-B语言，借助Rodin形式化建模和验证工具对联锁系统进行了形式化建模，并对Rodin工具生成的686条证明义务全部进行了证明。论文中对联锁系统功能进行了更为全面的形式化描述，特别地对列车进出站、调车转场、信号机故障、道岔故障、轨道区段故障、区段故障解锁，信号重开等功能进行了抽象化描述，同时考虑了超限绝缘节、条件检查等更为细致的站场条件。论文最后以典型的三股道站场对联锁模型进行了实例化，并以实例化后的模型对模型公理之间的矛盾性和死锁性进行了验证，同时使用BMotionWeb图形化工具对模型执行结果进行了可视化仿真。 论文中实现了联锁系统整体功能的抽象化捕述，联锁系统的形式化模型对应生成的686证明义务亦全部证明通过，同时可视化仿真的结果显示实例化的模型可完成联系系统功能。这表明EVENT-B语言适用于对铁路车站联锁系统类复杂系统进行形式化描述，可提高需求分析至程序实现过程中可靠性，为系统代码级开发的安全可靠性奠定了基础。此外，论文针对模型中AXIOM逻辑描述过于复杂，导致不能在ProB中正常执行的情形，提出了使用具体数据实例化模型的解决方案;同时利用定理的特性及实例化后的数据，对AXIOM之间的矛盾性及模型前后的一致性进行了验证和保证。文中提出的对联锁系统进行建模和验证的流程，对于提高联锁系统开发过程的可靠性具有一定的参考借鉴意义。 |
| 作者： | 张传东 |
| 专业： | 控制工程 |
| 导师： | 潘育山 |
| 授予学位： | 硕士 |
| 授予学位单位： | 西南交通大学 |
| 学位年度： | 2017 |
| 正文语种： | 中文 |
检索历史
应用推荐
