西南交通大学学报2013，Vol.48Issue(4)：708-714,7.DOI:10.3969/j.issn.0258-2724.2013.04.018
CTCS-3级列控系统临时限速建模与验证
Modeling and Verification of Temporary Speed Restriction of CTC-S3 Train Control System
摘要
Abstract
In order to meet the real-time performance requirement of a temporary speed restriction (TSR) system of Chinese train control system level 3 (CTCS-3),timed automata sub-models of each equipment of the train control system were established for the working process of TSR,and a timed automata network model was built through parallel composition of the sub-models to valuate the submodels using the parametric configuration of the specification of CTCS-3.Then,the properties of the TSR system such as safety and bounded liveness were expressed in Backus-Naur form (BNF) and validated through formal verification simulation using the UPPAAL integrated tool.The results show that compared with the parameters defined in the system specifications,the modified time parameters can fix the deadlock problem of the system,and improve the real-time performance of the TSR system on the premise of keeping the system properties such as safety and bounded liveness.The TSR system can respond to inputs within 5 s and meet the system specifications.关键词
CTCS-3级列控系统/临时限速/时间自动机/UPPAAL/实时性Key words
CTCS-3 train control system / TSR/ timed automata/ UPPAAL/ real-time performance分类
交通工程引用本文复制引用
袁磊,王俊峰,康仁伟,吕继东..CTCS-3级列控系统临时限速建模与验证[J].西南交通大学学报,2013,48(4):708-714,7.基金项目
国家863计划资助项目(2012AA112801) （2012AA112801）
本文工作得到轨道交通控制与安全国家重点实验室自主课题重点项目(RCS2011ZZ001)的资助. （RCS2011ZZ001）
