铁道标准设计Issue(3)：118-121,4.DOI:10.13238/j.issn.1004-2954.2015.03.028
移动授权的形式化建模与验证
Movement Authority Formal Modeling and Verification
摘要
Abstract
Compared with the traditional train control system, the communications-based train control system has been greatly improved either in function or in performance. In the development process of the system, system design flaws can be identified by modeling and verification so that the security and functionality of the system is guaranteed. Movement authority is a core function of CBTC system and is used to ensure the safe train interval. This paper, in the light of the generation principle of movement authority, uses timed automation modeling and UPPAAL verification for MA. The verification results show that the movement authority model so established can meet the requirements for safety and function. Thus, UPPAAL is capable of simulation and verification for complex real-time systems.关键词
CBTC/MA/时间自动机/UPPAALKey words
CBTC/MA/Timed Automation/UPPAAL分类
交通工程引用本文复制引用
贺欢欢,陈永刚,罗雅允,张彩珍..移动授权的形式化建模与验证[J].铁道标准设计,2015,(3):118-121,4.基金项目
甘肃省高校基本科研项目(620027) （620027）
