原文传递
列控系统TSRS形式化建模分析与验证
| 论文题名： | 列控系统TSRS形式化建模分析与验证 |
| 关键词： | 列控系统;临时限速;行车安全;时间自动机;仿真时序图 |
| 摘要： | 临时限速是指除线路规定的限速以外，由于施工、维修等原因引起的有计划的限速和由于自然灾害、设备故障等原因引起的突发限速。临时限速的设置关乎到提高运输效率和保障行车安全，随着列车速度的越来越快，对临时限速设置的安全性要求也越来越高。临时限速系统是列控系统的重要组成部分，是涉及到行车安全和运输效率的安全苛求系统。临时限速的工作流程具有严格的时序逻辑关系，体现出精确的时间约束特性。 针对临时限速系统的这些特性，有必要对其工作流程的实时性进行分析，采用形式化方法对系统的特性和行为进行建模描述，验证所产生的结果在逻辑和时间上的正确性及系统的实时性，从而发现系统规范的不完备性和模糊性，保证系统的安全性，为完善设计和开发提供重要的依据。 本文通过分析临时限速系统的结构，理清各设备之间的信息交互关系，结合临时限速系统的功能及调度命令的操作流程，说明各信息的交互方式;利用时间自动机理论对临时限速系统进行建模，并结合高铁CTC调度台分界口、CTCS等级转换区这两个特殊场景不同的工作流程建立各自的时间自动机模型。通过模型对系统的行为进行了精确的描述，避免了规范的不完备性和模糊性。提取临时限速系统的功能属性和性能属性要求并给出其BNF语法描述。在时间自动机模型的基础上，利用UPPAAL工具对模型进行时序逻辑的仿真，得到系统工作流程的仿真时序图，利用验证器对各模型的功能和性能属性进行验证。验证结果说明了系统的时间特性、受限活性和安全性。 |
| 作者： | 赵荣亮 |
| 专业： | 交通信息工程及控制 |
| 导师： | 王长林 |
| 授予学位： | 硕士 |
| 授予学位单位： | 西南交通大学 |
| 学位年度： | 2014 |
| 正文语种： | 中文 |
检索历史
应用推荐
