| 基于时间自动机的自主化ATP等级转换功能建模与验证 |
| |
| 引用本文： | 叶安君.基于时间自动机的自主化ATP等级转换功能建模与验证[J].城市轨道交通研究,2019,22(7):27-32,37. |
| |
| 作者姓名： | 叶安君 |
| |
| 作者单位： | 中铁第一勘察设计院集团有限公司,710043,西安 |
| |
| 摘 要： | 自主化ATP(列车自动保护)系统在国产化ATP系统的基础上,增加了一些新的功能需求。针对自主化ATP系统安全关键功能的安全性和正确性保障的问题,以自主化ATP系统中典型的C2等级转换C3等级的等级转换功能为研究对象,采用时间自动机形式化地分析等级转换功能的安全性、活性和实时性。研究时间自动机的数学理论基础,分析自主化ATP系统等级转换功能的逻辑和与其他系统的数据交互;采用时间自动机建模方法,从ATP、RBC(无线闭塞中心)和应答器3个方面,建立C2等级转换C3等级的时间自动机模型;研究自主化ATP系统等级转换功能需要满足的安全性、活性和实时性要求,利用UPPAAL软件验证等级转换功能的系统性质。结果表明,自主化ATP系统C2等级转换C3等级功能满足期望的系统需求。
|
| 关 键 词： | 高速铁路 时间自动机 ATP 等级转换 安全性 形式化验证 |
Modeling and Verification of ATP Level Transition Process Based on Timed Automata |
| |
| YE Anjun.Modeling and Verification of ATP Level Transition Process Based on Timed Automata[J].Urban Mass Transit,2019,22(7):27-32,37. |
| |
| Authors: | YE Anjun |
| |
| Institution: | (China Railway First Survey and Design Institute Group Co., Ltd., 710043, Xi′an, China) |
| |
| Abstract: | YE Anjun(China Railway First Survey and Design Institute Group Co., Ltd., 710043, Xi′an, China) |
| |
| Keywords: | high speed railway timed automata ATP level transition safety formal verification |
| 本文献已被 维普 万方数据 等数据库收录！ |
|
