Modeling of Handover Process in Operation Control System of Maglev Train Using Timed Automata

被引:0
|
作者
Gegerile [1 ]
Xu, Hongze [1 ]
Li, Yelei [1 ]
Liu, Jianfeng [1 ]
机构
[1] Beijing Jiaotong Univ, Sch Elect & Informat Engn, 3 Shangyuancun, Beijing, Peoples R China
关键词
timed auotomata; maglev train; operation control system; handover;
D O I
暂无
中图分类号
TP [自动化技术、计算机技术];
学科分类号
0812 ;
摘要
The OCS (operation control system) is playing a vital role in ensuring the high efficiency and safety of the maglev train. In this paper, we focused on modeling and verification of the handover process of OCS. After we analyzed the function and performance of the system, the process was modeled as a network of timed automata by the verification tool UPPAAL, which was synchronized to describe the communication establishment and massage exchange among subsystems. Then, some key properties that are vital to guarantee the correctness of the handover process were verified with the UPPAAL. Finally, the result shows that the handover process in operation control system of maglev train is provided with safety and restricted activity.
引用
收藏
页码:60 / 63
页数:4
相关论文
共 50 条
  • [1] Modeling and simulation for train control system using cellular automata
    KePing, Li
    Ziyou, Gao
    LiXing, Yang
    [J]. SCIENCE IN CHINA SERIES E-TECHNOLOGICAL SCIENCES, 2007, 50 (06): : 765 - 773
  • [3] Modeling and simulation for train control system using cellular automata
    KePing Li
    ZiYou Gao
    LiXing Yang
    [J]. Science in China Series E: Technological Sciences, 2007, 50 : 765 - 773
  • [4] Safety Processing Modeling of Train Location for High-Speed Maglev Operation Control System
    Chen, Yijun
    Xu, Zhongwei
    Zhao, Huahua
    Li, Zhangyang
    Chu, Pengzi
    [J]. CICTP 2021: ADVANCED TRANSPORTATION, ENHANCED CONNECTION, 2021, : 938 - 946
  • [5] The Verification of Temporary Speed Restriction of Train Control System Based on Timed Automata
    Lei Yuan
    Junfeng Wang
    Renwei Kang
    [J]. PROCEEDINGS OF THE INTERNATIONAL CONFERENCE ON COMPUTER, NETWORKS AND COMMUNICATION ENGINEERING (ICCNCE 2013), 2013, 30 : 355 - 358
  • [6] Modeling and supervisory control of timed automata
    Gouin, Alexia
    Ferrier, Jean-Louis
    [J]. Journal Europeen des Systemes Automatises, 1999, 33 (8-9): : 1093 - 1110
  • [7] Study on the operation control system framework for high-speed MAGLEV train
    Yang, Guang
    Tang, Zhen-Min
    [J]. Zhongguo Tiedao Kexue/China Railway Science, 2006, 27 (06): : 68 - 72
  • [8] PID Control to Maglev Train System
    Liu, Hengkun
    Zhang, Xiao
    Chang, Wensen
    [J]. 2009 INTERNATIONAL CONFERENCE ON INDUSTRIAL AND INFORMATION SYSTEMS, PROCEEDINGS, 2009, : 341 - 343
  • [9] GAUSSIAN PROCESS DYNAMIC MODELING AND BACKSTEPPING SLIDING MODE CONTROL FOR MAGNETIC LEVITATION SYSTEM OF MAGLEV TRAIN
    Sun, Yougang
    Wang, Sumei
    Lu, Yang
    Xu, Junqi
    [J]. JOURNAL OF THEORETICAL AND APPLIED MECHANICS, 2022, 60 (01): : 49 - 62
  • [10] Reliability Study of Maglev Automatic Train Operation System
    Yu Jianzhi
    Chen Yongsheng
    [J]. 2ND INTERNATIONAL SYMPOSIUM ON COMPUTER NETWORK AND MULTIMEDIA TECHNOLOGY (CNMT 2010), VOLS 1 AND 2, 2010, : 686 - 690