基于时间自动机的自主化ATP等级转换功能建模与验证
叶安君
Modeling and Verification of ATP Level Transition Process Based on Timed Automata
YE Anjun
-
作者信息:中铁第一勘察设计院集团有限公司，710043，西安
-
Affiliation:China Railway First Survey and Design Institute Group Co., Ltd., 710043, Xi′an, China
-
关键词:
-
Key words:
-
DOI:10.16037/j.1007-869x.2019.07.007
-
中图分类号/CLCN:U283.2
-
栏目/Col:研究报告
摘要:
自主化ATP(列车自动保护)系统在国产化ATP系统的基础上，增加了一些新的功能需求。针对自主化ATP系统安全关键功能的安全性和正确性保障的问题，以自主化ATP系统中典型的C2等级转换C3等级的等级转换功能为研究对象，采用时间自动机形式化地分析等级转换功能的安全性、活性和实时性。研究时间自动机的数学理论基础，分析自主化ATP系统等级转换功能的逻辑和与其他系统的数据交互；采用时间自动机建模方法，从ATP、RBC(无线闭塞中心)和应答器3个方面，建立C2等级转换C3等级的时间自动机模型；研究自主化ATP系统等级转换功能需要满足的安全性、活性和实时性要求，利用UPPAAL软件验证等级转换功能的系统性质。结果表明，自主化ATP系统C2等级转换C3等级功能满足期望的系统需求。
Abstracts:
Focusing on the safety and correctness of ATP (automatic train protection), on the basis of localized ATP, new functional requirements are added. Taking C2 level to C3 level transition process of ATP as the research object, timed automata is used to analyze its safety, activity and real-time performance. The mathematical foundation of timed automata is researched, the logic and interaction of ATP level transition functionality with other systems are analyzed; Using time automata modeling method, a C2 level to C3 level transition model is established from three aspects of ATP, RBC (radio block center) and the balise; The safety, activity and real-time requirements are extracted and verified by UPPAAL software. The result shows that the C2 level to C3 level transition process of ATP could meet expected system requirements.
引文 / Ref:
叶安君.基于时间自动机的自主化ATP等级转换功能建模与验证[J].城市轨道交通研究，2019，22(07):27.
YE Anjun.Modeling and verification of ATP level transition process based on timed automata[J].Urban Mass Transit，2019，22(07)：37.
YE Anjun.Modeling and verification of ATP level transition process based on timed automata[J].Urban Mass Transit，2019，22(07)：37.
过刊浏览
资料下载
友情链接