基于UPPAAL的列控系统临时限速建模与验证  

UPPAAL-based modeling and verification of temporary speed restriction in train control system

作　　者：宋莉 刘伯鸿[1] SONG Li;LIU Bohong(College of Automation&Electrical Engineering,Lanzhou Jiaotong University,Lanzhou 730070,China)

机构地区：[1]兰州交通大学自动化与电气工程学院,兰州730070

出　　处：《铁路计算机应用》2020年第5期12-16,共5页Railway Computer Application

基　　金：中国铁路总公司科技研究开发计划项目(2017X010-E)。

摘　　要：临时限速系统是列控系统的重要组成部分,是符合"故障–安全"准则的安全苛求系统。文章基于临时限速技术规范和时间自动机理论,分析临时限速系统的组成结构,提取其功能和性能约束,利用UPPAAL工具对其信息交互行为进行建模仿真,验证该系统的实时性,为进一步完善临时限速系统的设计与开发提供参考。As an important part of the train control system,the temporary speed restriction system is a safety-critical one that meets fail-safe criteria.Based on the technical specification on temporary speed restriction and the theory of timed automata,this paper analyzed the composition and structure of the temporary speed restriction system,extracted its function and performance constraints for modeling and simulating its data interaction behaviors by using UPPAAL tool to verify its real-time performance,offering reference for further improving the design and development of the temporary speed restriction system.

关 键 词：建模与验证 临时限速 安全苛求系统 故障-安全准则 时间自动机 UPPAAL 

分 类 号：U284.482[交通运输工程—交通信息工程及控制] TP39[交通运输工程—道路与铁道工程]