基于时间自动机的CBI道岔转换时间建模与验证

详细信息

Modeling and verification of CBI switch transaction time based on timed automata

School of Information Science and Technology, Southwest Jiaotong University, Chengdu 610031, China

摘要: 针对CBTC计算机联锁安全性十分重要的问题，介绍时间自动机理论，分析CBTC计算机联锁系统的结构和与传统联锁系统的区别，以CBTC联锁系统的道岔转换功能为例，采用UPPAAL建立了道岔转换模型，分析模型的安全需求。表明了在联锁系统开发过程中采用基于时间自动机建模与验证的方法的可行性和有效性。
- 时间自动机 /
- 计算机联锁 /
- 建模 /
- 验证
Abstract: Focusing on the problem that the safety of CBTC computer based interlocking is critical, this article introduced the theory of timed automata, analyzed the architecture and differences between CBTC computer based interlocking system and traditional interlocking system, took an example of switch transaction, switch transaction model was established by using UPPAAL. The security requirements of the model were also analyzed, which showed the feasibility and effectiveness of the modeling and verification methods based on timed automata, during the process of developing computer based interlocking system.
- timed automata /
- computer based interlocking (CBI) /
- modeling /
- verification

[1]	Pengfei Sun,Simon Collart-dutilleul, Philippe Bon, A Model Pattern of Railway Interlocking System by Petri Nets[C].International Conference on Models and Technologies for Intelligent Transportation Systems (MT-ITS), 2015.
[2]	郭华.UPPAAL_ 一种适合自动验证实时系统的工具[J].微计算机信息，2006，22（5）：1-2.
[3]	孙全勇. 时间自动机及其应用研究[D]. 哈尔滨：哈尔滨工程大学，2006.
[4]	James L. Rash Christopher A. Rouff Walt Truszkowski Diana Gordon Michael G. Hinchey. Formal Approaches toAgent-Based Systems[Z]. Springer,2000,117: 120.
[5]	杨淘. 基于CBTC 系统的联锁逻辑研究[D]. 成都：西南交通大学，2014.
[6]	王观宁. 基于UPPAAL 的联锁进路控制流程建模与验证[D].北京：北京交通大学，2009.