• ISSN 0258-2724
  • CN 51-1277/U
  • EI Compendex
  • Scopus
  • Indexed by Core Journals of China, Chinese S&T Journal Citation Reports
  • Chinese S&T Journal Citation Reports
  • Chinese Science Citation Database
Volume 26 Issue 4
Aug.  2013
Turn off MathJax
Article Contents
Journal of Southwest Jiaotong University  > 2013  >  26(4): 708-714.
YUAN Lei, WANG Junfeng, KANG Renwei, LÜ, Jidong. Modeling and Verification of Temporary Speed Restriction of CTC-S3 Train Control System[J]. Journal of Southwest Jiaotong University, 2013, 26(4): 708-714. doi: 10.3969/j.issn.0258-2724.2013.04.018
Citation: YUAN Lei, WANG Junfeng, KANG Renwei, LÜ, Jidong. Modeling and Verification of Temporary Speed Restriction of CTC-S3 Train Control System[J]. Journal of Southwest Jiaotong University, 2013, 26(4): 708-714. doi: 10.3969/j.issn.0258-2724.2013.04.018
shu

Modeling and Verification of Temporary Speed Restriction of CTC-S3 Train Control System

doi: 10.3969/j.issn.0258-2724.2013.04.018
  • Received Date: 25 Aug 2012
  • Publish Date: 25 Aug 2013
    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 sub-models 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.

     

    • FullText(HTML)
  • loading
    • References(19)
  • 郭震. CTCS各级系统中临时限速技术运用的探讨[J]. 科技信息,2011(16): 111-112. GUO Zhen. Exploration of temporary speed restriction technology application at all levels in CTCS[J]. Science and Technology Information, 2011(16): 111-112.
    黄媛媛,董昱,赵宇坤. 临时限速对列车运行影响的仿真研究[J]. 铁道通信信号,2011,47(1): 13-15. HUANG Yuanyuan, DONG Yu, ZHAO Yukun. Simulation study of temporary speed restriction on train operation[J]. Railway Signalling & Communication, 2011, 47(1): 13-15.
    古天龙. 软件开发的形式化方法[M]. 北京:高等教育出版社,2005: 4-24.
    吕继东. 列车运行控制系统分层形式化建模与验证分析[D]. 北京:北京交通大学,2011.
    曹源,唐涛,徐天华,等. 形式化方法在列车运行控制系统中的应用[J]. 交通运输工程学报,2010,10(1): 112-126. CAO Yuan, TANG Tao, XU Tianhua, et al. Application of formal methods in train control system[J]. Journal of Traffic and Transportation Engineering, 2010, 10(1): 112-126.
    周清雷,姬莉霞. 基于时间自动机的道岔自动控制研究[J]. 控制工程, 2004,11(增刊): 146-149. ZHOU Qinglei, JI Lixia. On automatic turnout control based on timed automata[J]. Control Engineering of China, 2004, 11(Sup.): 146-149.
    ALUR R, DILL D L. A theory of timed automata[J]. Theoretical Computer Science, 1994, 126 : 183-235.
    OLDEROG E R, DIERKS H. Real-time systems[M]. London: Cambridge University Press, 2008: 137-146.
    梁楠,王海峰. 基于SPN的CTCS-3级列控系统RBC实时性能分析[J]. 铁道学报,2011,33(2): 67-71. LIANG Nan, WANG Haifeng. Real-time performance analysis of RBC system for ctcs lever 3 using stochastic Petri networks[J]. Journal of the China Railway Society, 2011, 33(2): 67-71.
    曹源. 高速铁路列车运行控制系统的形式化建模与验证方法研究[D]. 北京:北京交通大学,2011.
    吴琼,邵志清,刘刚. 基于着色时间Petri网的实时系统的形式验证[J]. 计算机科学,2008,35(7): 257-260. WU Qiong, SHAO Zhiqing, LIU Gang. Formal verification of real-time system based on colored time Petri net[J]. Computer Science, 2008, 35(7): 257-260.
    吕继东,唐涛. 高速铁路列控系统运营场景实时性的建模与验证[J]. 铁道学报,2011,33(6): 54-61. LV Jidong, TANG Tao. Modeling and verification of time constraints of operation scenarios of high-speed train control system[J]. Journal of the China Railway Society, 2011, 33(6): 54-61.
    承向军,应志鹏,杜鹏. 高速列车ATP控车模式的形式化模型与安全分析[J]. 中国安全科学学报,2008,18(3): 28-32. CHENG Xiangjun, YING Zhipeng, DU Peng. Formalization model of high speed trains in ATP control and its safety analysis[J]. China Safety Science Journal, 2008, 18(3): 28-32.
    曹源,唐涛,罗丹. 列车运行控制系统设计正确性的验证方法[J]. 西南交通大学学报,2010,45(4): 574-579. CAO Yuan, TANG Tao, LUO Dan. Method for verifying the correctness of train control system design[J]. Journal of Southwest Jiaotong University, 2010, 45(4): 574-579.
    XU Ke, PATTERSSON P, SIERSZECKI K. Verification of COMDES-Ⅱ systems using UPPAAL with model transformation[C]//The 14th IEEE International Conference on Embedded and Real-Time Computing Systems and Applications. Los Alamitos: IEEE Computer Society, 2008: 153-160.
    HESSEL A, LARSEN K G, MIKUCIONIS M. Testing real-time systems using UPPAAL[J]. Lecture Notes in Computer Science, 2008, 4949: 77-117.
    BEHRMANN G, LARSEN K G. UPPAAL-present and future[C]//Proceedings of the 40th IEEE Conference on Decision and Control. New York: IEEE, 2001: 2881-2886.
    孙全勇. 时间自动机及其应用研究[D]. 哈尔滨:哈尔滨工程大学,2007.
    铁道部科学技术司,铁道部运输局. CTCS-3级列控系统标准规范系列:客运专线列控系统临时限速技术规范[M].北京:中国铁道出版社,2008: 6-9,27-30.
    • Relative Articles
    • Supplements(0)
    • Cited By
  • 加载中

Catalog

    通讯作者: 陈斌, bchen63@163.com
    • 1. 

      沈阳化工大学材料科学与工程学院 沈阳 110142

    1. 本站搜索
    2. 百度学术搜索
    3. 万方数据库搜索
    4. CNKI搜索
    Get Citation
    PDF
    XML
    Article views(1042) PDF downloads(341) Cited by()
    Proportional views
    Related

    Copyright © 2009 Journal of Southwest Jiaotong University

    Address: RM449 & 451, Administrative Building, Xipu Campus, Southwest Jiaotong University Western Hi-tech Zone, Chengdu, Sichuan 611756, P. R. China

    Tel: 028-66367562Fax: 028-66366552Email: xbz@home.swjtu.edu.cn

    Supported by: Beijing Renhe Information Technology Co. Ltd  support: info@rhhz.net

    /

    DownLoad:  Full-Size Img  PowerPoint
    Return
    Return