Formal modeling and verification of CTCS-3 train control on-board equipment
CSTR:
Author:
Affiliation:

1.School of Automation and Electrical Engineering, Lanzhou JiaoTong University, Lanzhou 730070, P. R. China;2.Gansu Research Center of Automation Engineering Technology for Industry &Transportation, Lanzhou JiaoTong University, Lanzhou 730070, P. R. China

Fund Project:

Supported by National Natural Science Foundation of China(U2268206).

  • Article
  • | |
  • Metrics
  • |
  • Reference [16]
  • |
  • Related [20]
  • |
  • Cited by
  • | |
  • Comments
    Abstract:

    The CTCS-3 train control system is subject to stringent safety requirements, with the train control on-board equipment serving as its core. This equipment plays a vital role in operating and controlling the train, ensuring the overall safety of train operation. In this study, the information interaction between CTCS-3 train control on-board devices and the work mode conversion rules in the on-boar safety computer was analyzed. To establish a comprehensive model, colored Petri nets (CPN) were used, enabling the construction of an information interaction model and work mode transformation model for the on-board equipment. To validate the model’s effectiveness, the ASK-CTL branching sequence logic formula was used to verify its performance concerning dead identification, deadlock and transferability under various working modes. The results show that the CPN model conforms to the system specification requirements, adhering to the expected process and rules. This research provides valuable ingishgts and serves as a reference for the design of the relevant security demanding systems.

    Reference
    [1] 张曙光. CTCS-3级列控系统总体技术方案[M]. 北京: 中国铁道出版社, 2008: 26-37.Zhang S G. Overall technical scheme of CTCS-3 train control system[M]. Beijing: China Railway Publishing House, 2008: 26-37.(in Chinese)
    [2] Hr Hardi, Michael M. Modelling functionality of train control system using petri nets[C]//Fm-rail-bok Workshop. Madrid: DLR, 2013:1-6.
    [3] 何文锋. 基于UML的CTCS-3级列控车载设备建模、仿真和测试研究[D]. 北京: 北京交通大学, 2009.He W F. Research on modeling, simulation and testing of CTCS-3 train control vehicle equipment based on UML[D].Beijing: Beijing Jiaotong University, 2009. (in Chinese)
    [4] 曹加云. 基于时间自动机的CTCS-3级列控车载设备建模与验证[D]. 成都: 西南交通大学, 2010.Cao J Y. Modeling and verification of CTCS-3 train control vehicle equipment based on time automata[D].Chengdu: Southwest Jiaotong University, 2010. (in Chinese)
    [5] 牟小玲, 丁晓明, 张望. 基于Petri网的测试用例生成研究进展[J]. 重庆交通大学学报(自然科学版), 2012, 31(1): 163-167.Mu X L, Ding X M, Zhang W. Research progress in test case generation based on petri nets[J]. Journal of Chongqing Jiaotong University (Natural Science), 2012, 31(1): 163-167.(in Chinese)
    [6] 中国铁路总公司. CTCS-3级列车运行控制系统[M]. 北京: 中国铁道出版社, 2013.China Railway Corporation. CTCS-3 train operation control system [M]. Beijing: China Railway Publishing House, 2013.
    [7] Wang R, Zheng W, Liang C, et al. An integrated hazard identification method based on the hierarchical Colored Petri Net[J]. Safety Science, 2016, 88: 166-179.
    [8] 铁道部科技司. CTCS-3级列控系统标准规范-CTCS-3级列控系统系统需求规范(SRS)(第一册)[S]. 北京: 中国铁道出版社, 2009.Department of Science and Technology.Ministry of railways standard specification for CTCS-3 class train control system (SRS) (volume 1) [S]. Beijing: China Railway Publishing House, 2009.(in Chinese)
    [9] 马国富, 刘文良, 周建勇, 等. 基于ASK-CTL的有色Petri网模型检验算法研究[J]. 计算机应用与软件, 2015, 32(10): 302-305, 333.Ma G F, Liu W L, Zhou J Y, et al. Study on coloured petri net model checking based on ask-ctl[J]. Computer Applications and Software, 2015, 32(10): 302-305, 333.(in Chinese)
    [10] 赵晓宇, 杨志杰, 吕旌阳. 基于有色Petri网的车载设备模式转换测试序列生成方法[J]. 中国铁道科学, 2017, 38(4): 115-122.Zhao X Y, Yang Z J, Lv S Y. A Method for generating test sequence of on-board equipment mode conversion based on colored petri nets [J]. China Railway Science, 2017, 38(4): 115-122.(in Chinese)
    [11] 胡少强. 基于STPA和有色Petri网的列控系统安全分析[D]. 北京: 北京交通大学, 2018.Hu S Q. Safety analysis of train control system based on STPA and colored petri net[D].Beijing: Beijing Jiaotong University, 2018. (in Chinese)
    [12] Koh K Y, Seong P H. SMV model-based safety analysis of software requirements[J]. Reliability Engineering & System Safety, 2009, 94(2): 320-331.
    [13] 赵伟慧. 基于场景的列控车载设备测试用例自动生成方法研究[D]. 北京: 北京交通大学, 2014.Zhao W H. Research on automatic generation method of test cases for train control vehicle equipment based on scene[D].Beijing: Beijing Jiaotong University, 2014. (in Chinese)
    [14] Lh V, Hong L. Formal development and verification of railway control systems- in the context of ERTMS/ETCS level 2[D]. Copenhagen: DTU, 2015:13-20.
    [15] Huang W L, Peleska J. Complete model-based equivalence class testing[J]. International Journal on Software Tools for Technology Transfer, 2016, 18(3): 265-283.
    [16] Jensen K, Kristensen L M, Wells L. Coloured Petri Nets and CPN tools for modelling and validation of concurrent systems[J]. International Journal on Software Tools for Technology Transfer, 2007, 9(3/4): 213-254.
    Cited by
Get Citation

何涛,韩敬佳.CTCS-3级列控车载设备的形式化建模与验证[J].重庆大学学报,2023,46(9):120~129

Copy
Related Videos

Share
Article Metrics
  • Abstract:324
  • PDF: 925
  • HTML: 143
  • Cited by: 0
History
  • Received:June 09,2020
  • Online: September 25,2023
Article QR Code