基于Event-B和MAS的车站进路联锁控制逻辑的形式化方法研究
发布时间：2022-02-18 20:07
随着我国铁路事业的飞速发展,安全、高速成为铁路系统的硬性标准。我国在引进和借鉴欧洲ETCS列控系统的基础上,研发了拥有自主产权的CTCS-3级中国列车控制系统。计算机联锁系统则是保证列车行车安全的基础设备,主要是利用联锁软件完成联锁功能的一种安全苛求性系统,符合“故障-安全”原则。车站联锁控制直接关系到行车安全,也影响到车站作业的效率及行车组织工作,因此联锁系统在不断更新和改进。传统的联锁软件开发很多是用非形式化语言和自然语义来描述的,主要应用于软件工程的需求分析方法,在设计、分析和测试上已无法满足计算机联锁系统的安全需求。所以使用形式化的方法对联锁系统进行规范和说明,不仅可以提高计算机联锁软件的质量,也有利于进行更为严格的测试。计算机联锁主要是由微型计算机的软件、硬件和一些电子、继电器件组成的,具有高可靠性和安全性的实时控制系统,联锁的意义就在于进路控制过程的表述。通过结合6502继电器的功能描述,对车站进路联锁控制逻辑进行完整说明,使用具有严谨数学语义的形式化方法对联锁系统的安全规范进行验证。本文在学习和研究铁路联锁技术的基础上,以车站进路为场景,运用形式化方法Event-B和多智...
【文章来源】：兰州交通大学甘肃省
【文章页数】：77 页
【学位级别】：硕士
【文章目录】：
摘要
Abstract
引言
1 绪论
1.1 研究背景
1.2 研究目的和意义
1.3 车站联锁国内外研究综述
1.4 论文主要内容及结构框架
2 形式化描述与验证方法理论
2.1 形式化方法
2.1.1 形式化描述
2.1.2 形式化方法验证和应用
2.2 Event-B方法及Rodin平台
2.2.1 Event-B基本结构
2.2.2 Event-B的数学体系
2.2.3 Event-B模型精化和证明义务
2.2.4 RODIN平台
2.3 MAS的方法理论
2.3.1 Agent的概述
2.3.2 多智能体系统(Multi-Agent System,MAS)
2.4 本章小结
3 联锁的安全规范及逻辑语义描述
3.1 铁路联锁安全规范的提取方法
3.1.1 进路控制安全规范
3.1.2 信号控制安全规范
3.1.3 道岔控制安全规范
3.2 联锁规范的逻辑语义描述
3.3 本章小结
4 基于Event-B的联锁安全规范的描述和验证
4.1 联锁系统安全规范Event-B描述方法
4.1.1 联锁规范形式化描述及精化策略
4.1.2 车站进路联锁逻辑的Event-B初始模型
4.1.3 车站进路控制的Event-B建模分析
4.1.4 车站进路联锁控制的Event-B模型精化和验证
4.2 车站进路联锁Event-B验证方法
4.3 本章小结
5 基于MAS和Event-B的分布式联锁安全的描述
5.1 分布式实时系统
5.2 MAS的体系结构
5.3 联锁安全描述
5.3.1 Multi-Agent联锁层的安全规范描述
5.3.2 Event-B的模型规范
5.3.3 精化
5.4 本章小结
结论
致谢
参考文献
攻读学位期间的研究成果
【参考文献】：
期刊论文
[1]城轨综合监控系统的多Agent模型[J]. 董存祥. 铁道工程学报. 2013(12)
[2]基于Event-B的计算机联锁安全规范描述与验证[J]. 张越,王海峰. 铁路计算机应用. 2013(11)
[3]高速铁路信号设备动态管理方案研究[J]. 方明亮,胡恩华,魏盛昕,涂鹏飞. 铁道通信信号. 2013(03)
[4]CTCS-3级列控系统规范的建模与形式化验证方法研究[J]. 谢雨飞,唐涛,徐田华,赵林. 铁道学报. 2011(07)
[5]高速铁路列控车载设备的发展[J]. 王馨. 铁路通信信号工程技术. 2010(05)
[6]形式化方法在列车运行控制系统中的应用[J]. 曹源,唐涛,徐田华,穆建成. 交通运输工程学报. 2010(01)
[7]基于Repast平台的多Agent仿真建模研究[J]. 蒋慧超,韦兆文. 计算机技术与发展. 2008(11)
[8]采用DFS策略的进路搜索算法研究[J]. 胡媛,魏宗寿. 铁路计算机应用. 2007(09)
[9]计算机联锁软件的Z规格说明[J]. 王铁江,郦萌. 铁道学报. 2003(04)
[10]我国铁路信号系统的现状与发展[J]. 姚丽娟. 铁道通信信号. 2003(04)
博士论文
[1]基于角色的多智能体社会模型研究与应用[D]. 何汉明.西北工业大学 2006
硕士论文
[1]基于CSP的城轨CBTC联锁逻辑形式化建模与验证[D]. 马慧.北京交通大学 2013
[2]基于Event-B的软件需求形式化建模技术的研究[D]. 陈志慧.电子科技大学 2013
[3]高速铁路列车运行调整问题研究[D]. 吴丽然.西南交通大学 2011
[4]CTCS-3级计算机联锁系统仿真实现[D]. 王亚东.西南交通大学 2011
[5]B方法在配电自动化系统中的应用研究[D]. 孟芸.河南大学 2010
[6]高速列车运行控制系统仿真[D]. 廖丽军.北京交通大学 2009
[7]基于人工智能的知识发现[D]. 臧其事.华东师范大学 2008
[8]基于B语言与TPN集成的形式化方法[D]. 姜梦稚.华东师范大学 2006
[9]铁路信号系统的Petri网建模与分析研究[D]. 钟文燕.西南交通大学 2005
本文编号：3631470
【文章来源】：兰州交通大学甘肃省
【文章页数】：77 页
【学位级别】：硕士
【文章目录】：
摘要
Abstract
引言
1 绪论
1.1 研究背景
1.2 研究目的和意义
1.3 车站联锁国内外研究综述
1.4 论文主要内容及结构框架
2 形式化描述与验证方法理论
2.1 形式化方法
2.1.1 形式化描述
2.1.2 形式化方法验证和应用
2.2 Event-B方法及Rodin平台
2.2.1 Event-B基本结构
2.2.2 Event-B的数学体系
2.2.3 Event-B模型精化和证明义务
2.2.4 RODIN平台
2.3 MAS的方法理论
2.3.1 Agent的概述
2.3.2 多智能体系统(Multi-Agent System,MAS)
2.4 本章小结
3 联锁的安全规范及逻辑语义描述
3.1 铁路联锁安全规范的提取方法
3.1.1 进路控制安全规范
3.1.2 信号控制安全规范
3.1.3 道岔控制安全规范
3.2 联锁规范的逻辑语义描述
3.3 本章小结
4 基于Event-B的联锁安全规范的描述和验证
4.1 联锁系统安全规范Event-B描述方法
4.1.1 联锁规范形式化描述及精化策略
4.1.2 车站进路联锁逻辑的Event-B初始模型
4.1.3 车站进路控制的Event-B建模分析
4.1.4 车站进路联锁控制的Event-B模型精化和验证
4.2 车站进路联锁Event-B验证方法
4.3 本章小结
5 基于MAS和Event-B的分布式联锁安全的描述
5.1 分布式实时系统
5.2 MAS的体系结构
5.3 联锁安全描述
5.3.1 Multi-Agent联锁层的安全规范描述
5.3.2 Event-B的模型规范
5.3.3 精化
5.4 本章小结
结论
致谢
参考文献
攻读学位期间的研究成果
【参考文献】：
期刊论文
[1]城轨综合监控系统的多Agent模型[J]. 董存祥. 铁道工程学报. 2013(12)
[2]基于Event-B的计算机联锁安全规范描述与验证[J]. 张越,王海峰. 铁路计算机应用. 2013(11)
[3]高速铁路信号设备动态管理方案研究[J]. 方明亮,胡恩华,魏盛昕,涂鹏飞. 铁道通信信号. 2013(03)
[4]CTCS-3级列控系统规范的建模与形式化验证方法研究[J]. 谢雨飞,唐涛,徐田华,赵林. 铁道学报. 2011(07)
[5]高速铁路列控车载设备的发展[J]. 王馨. 铁路通信信号工程技术. 2010(05)
[6]形式化方法在列车运行控制系统中的应用[J]. 曹源,唐涛,徐田华,穆建成. 交通运输工程学报. 2010(01)
[7]基于Repast平台的多Agent仿真建模研究[J]. 蒋慧超,韦兆文. 计算机技术与发展. 2008(11)
[8]采用DFS策略的进路搜索算法研究[J]. 胡媛,魏宗寿. 铁路计算机应用. 2007(09)
[9]计算机联锁软件的Z规格说明[J]. 王铁江,郦萌. 铁道学报. 2003(04)
[10]我国铁路信号系统的现状与发展[J]. 姚丽娟. 铁道通信信号. 2003(04)
博士论文
[1]基于角色的多智能体社会模型研究与应用[D]. 何汉明.西北工业大学 2006
硕士论文
[1]基于CSP的城轨CBTC联锁逻辑形式化建模与验证[D]. 马慧.北京交通大学 2013
[2]基于Event-B的软件需求形式化建模技术的研究[D]. 陈志慧.电子科技大学 2013
[3]高速铁路列车运行调整问题研究[D]. 吴丽然.西南交通大学 2011
[4]CTCS-3级计算机联锁系统仿真实现[D]. 王亚东.西南交通大学 2011
[5]B方法在配电自动化系统中的应用研究[D]. 孟芸.河南大学 2010
[6]高速列车运行控制系统仿真[D]. 廖丽军.北京交通大学 2009
[7]基于人工智能的知识发现[D]. 臧其事.华东师范大学 2008
[8]基于B语言与TPN集成的形式化方法[D]. 姜梦稚.华东师范大学 2006
[9]铁路信号系统的Petri网建模与分析研究[D]. 钟文燕.西南交通大学 2005
本文编号：3631470
本文链接：https://www.wllwen.com/shekelunwen/ljx/3631470.html
