• 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 56 Issue 3
Jun.  2021
Turn off MathJax
Article Contents
Abstract
References
Journal of Southwest Jiaotong University  > 2021  >  56(3): 587-593, 610.
YANG Jihua, YAN Changbin. Wear Predication of Tunnel Boring Machine Cutters Based on In-situ Measured Data[J]. Journal of Southwest Jiaotong University, 2019, 54(6): 1283-1292. doi: 10.3969/j.issn.0258-2724.20170677
Citation: WANG Keming, WANG Xia, CHENG Peng, LIU Ning, ZHANG Chuandong. Formal Method for Behavior Verification and Data Validation of Station Interlocking System[J]. Journal of Southwest Jiaotong University, 2021, 56(3): 587-593, 610. doi: 10.3969/j.issn.0258-2724.20191182
shu

Formal Method for Behavior Verification and Data Validation of Station Interlocking System

doi: 10.3969/j.issn.0258-2724.20191182
  • Received Date: 16 Dec 2019
  • Rev Recd Date: 08 Jun 2020
    • Available Online: 24 Aug 2020
  • Publish Date: 15 Jun 2021
    Abstract
  • Station interlocking system is a typical safety-critical system driven by data, which needs to verify the system behavior and confirm the correctness of data in the development. After analyzing the design specifications of the interlocking system, the initial system model was built automatically by the UML (unified modeling language) diagram, with the system properties and event flows described by Event-B language on RODIN platform. Subsequently, the refinement policy was used for hierarchical modeling, and the proof obligations of each layer were proved by theorem and the properties of the system attributions were verified. Thus, a reliable universal function model was obtained. Using a real station yard, the axioms of the model were proved and the interlocking data were validated as well. According to the formal verification and data validation in a given scenario, the subtle defects generated in the analysis of the system requirements could be found and corrected. Finally, the functional simulation and acceptance testing confirmed the correctness of the general model and the interlock data. This method not only improves the accuracy and hierarchy of the model-based development, but also verifies the universal behavior state of the system. Combined with axiomatic verification, the validation of interlocking data is realized. The function scenario can be simulated and tested based on the model, which can further improve the reliability of the universal function prototype of the system.

     

    • FullText(HTML)
    • References(11)
  • 王恪铭,王峥. 基于形式化方法的道口控制系统规范建模与验证[J]. 西南交通大学学报,2019,54(3): 573-578,603.

    WANG Keming, WANG Zheng. Modeling and verification of control system specification for railway level crossings based on formal method[J]. Journal of Southwest Jiaotong University, 2019, 54(3): 573-578,603.
    International Electrotechnical Commision. Functional safety of electrical/electronic/programmable electronic safety-reared systems: IEC 61508[S]. Geneva: European Committee for Electrotechnical Standardization. 2005.
    KHAN U, AHMAD J, SAEED T, et al. On the real time modeling of interlocking system of passenger lines of Rawalpindi Cantt train station[J]. Complex Adaptive Systems Modeling, 2016, 4(1): 1-33. doi: 10.1186/s40294-016-0028-5
    VU L H, HAXTHAUSEN A E, PELESKA J. Formal modelling and verification of interlocking systems featuring sequential release[J]. Science of Computer Programming, 2017, 133: 91-115. doi: 10.1016/j.scico.2016.05.010
    BONACCHI A, FANTECHI A, BACHERINI S, et al. Validation process for railway interlocking systems[J]. Science of Computer Programming., 2016, 128: 2-21. doi: 10.1016/j.scico.2016.04.004
    HANSEN D, SCHNEIDER D, LEUSCHEL M. Using B and ProB for data validation projects[C]//Inernational Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z. [S.l.]: Springer, 2016: 167-182.
    ABRIAL J R. Train system[M]//Modeling in Event-B. Cambridge: Cambridge University Press, 2013: 508-549.
    国家铁路局. 铁路车站计算机联锁技术条件: TB/T 3027—2015[S]. 北京: 中国铁道出版社. 2015.
    张传东. EVENT-B方法在铁路车站联锁规范形式化建模与验证中的应用研究[D]. 成都: 西南交通大学, 2017.
    ZHANG Chuandong, WANG Keming, WANG Xia, et al. Interlocking data[DB/OL]. [2019-08-16]. https://github.com/abidefei/Model_Verification_Data_Validation_Interlocking_EventB.
    SNOOK C, HOANG T S, DGHYAM D, et al. Behaviour-driven formal model development[M]//Formal Methods and Software Engineering. Cham: Springer International Publishing, 2018: 21-36.
    • Relative Articles

  • Relative Articles

    [1]SHI Zengshu, LI Yao, GUO Jin, ZHANG Yadong. Testing Modeling Method for Engineering Testing of High-Speed Railway Signaling System[J]. Journal of Southwest Jiaotong University, 2024, 59(5): 1023-1033. doi: 10.3969/j.issn.0258-2724.20220674
    [2]WANG Xia, WANG Keming, XU Yang, TANG Weijian. Safety Design of Level Crossing Control System Based on Formal Method[J]. Journal of Southwest Jiaotong University, 2023, 58(1): 109-116. doi: 10.3969/j.issn.0258-2724.20210656
    [3]LI Yao, ZHANG Xiaoxia, GUO Jin, ZHANG Yadong. Modeling Method for Testing Railway Signal System Software[J]. Journal of Southwest Jiaotong University, 2022, 57(2): 392-400, 424. doi: 10.3969/j.issn.0258-2724.20200530
    [4]LI Yao, ZHANG Xiaoxia, GUO Jin, ZHANG Yadong. Testing Modeling Method for Safety Critical Function of High-Speed Railway Signal System[J]. Journal of Southwest Jiaotong University, 2022, 57(1): 28-35, 45. doi: 10.3969/j.issn.0258-2724.20200378
    [5]WEI Baiquan, LÜ Jidong, CHEN Kexing, TANG Tao, WANG Wei. Mutation Timed Automata with Input and Output-Based Method of Generating Test Suites for Chinese Train Control System Level 3[J]. Journal of Southwest Jiaotong University, 2020, 55(5): 937-945, 962. doi: 10.3969/j.issn.0258-2724.20180078
    [6]CAO Feng, XU Yang, CHEN Shuwei, WU Guanfeng, CHANG Wenjing. Application of Multi-Clause Synergized Deduction in First-Order Logic Automated Theorem Proving[J]. Journal of Southwest Jiaotong University, 2020, 55(2): 401-408, 427. doi: 10.3969/j.issn.0258-2724.20180800
    [7]WANG Keming, WANG Zheng. Modeling and Verification of Control System Specification for Railway Level Crossings Based on Formal Method[J]. Journal of Southwest Jiaotong University, 2019, 54(3): 573-578, 603. doi: 10.3969/j.issn.0258-2724.20180607
    [8]CHEN Yonghong, CHEN Yan, WANG Jinge, ZHANG Guanghui. Performance Testing of Planar Internal Gear Primary-Enveloping Crown Worm Drive[J]. Journal of Southwest Jiaotong University, 2015, 28(4): 725-731. doi: 10.3969/j.issn.0258-2724.2015.04.023
    [9]WANG Xuemei, NI Wenbo. Strapdown Inertial Measurement Method Based on Data Fusion Technique and Its Application to Railway Track[J]. Journal of Southwest Jiaotong University, 2014, 27(1): 8-14,51. doi: 10.3969/j.issn.0258-2724.2014.01.002
    [10]LI Xiaozhen, LIU Quanmin, ZHANG Xun, ZHANG Zhijun. Measurement and Theoretical Analysis of Vehicle-Induced Vibration on Elevated Railway Station[J]. Journal of Southwest Jiaotong University, 2014, 27(4): 612-618. doi: 10.3969/j.issn.0258-2724.2014.04.008
    [11]WEN Ruizhi, REN Yefei, QI Wenhao, LU Tao, YANG Zhenyu, SHAN Zhendong, WANG Yunlong. Maximum Acceleration Recording from Lushan Earthquake on April 20, 2013[J]. Journal of Southwest Jiaotong University, 2013, 26(5): 783-791. doi: 10.3969/j.issn.0258-2724.2013.05.001
    [12]ZHANG Bangcheng, LU Hongwei, WANG Zhanli, ZHOU Zhijie. Design of Electrical Control System of Test Machine of Automobile Clutch Centre Plate[J]. Journal of Southwest Jiaotong University, 2009, 22(1): 106-111.
    [13]PANZhou-ping, ZHANGLi-min. Design of Continuous Wheel/Rail Force Measurement System[J]. Journal of Southwest Jiaotong University, 2004, 17(1): 69-72.
    [14]YANG Guang, QIUJing, WENXi-sen, LIU Guan-jun. Mathematical Model Analysis of False Alarm in Mechatronics Built-in Test Systems[J]. Journal of Southwest Jiaotong University, 2003, 16(5): 581-583.
    [15]YANGJiang, LI Zhi. Analysis of Data Validity in SimulationModel Validation[J]. Journal of Southwest Jiaotong University, 2003, 16(3): 258-262.
    [16]ZHANGCui一fang, HUANGHai一yu, DENGChang一yan. AnoverallSehemeforHighTemPeratureSuPercondueting MaglevMeasurementSystem 一DataAequisitionandMotionControl[J]. Journal of Southwest Jiaotong University, 2001, 14(4): 440-443.
    • Supplements(0)
    • Cited By

  • Cited by

    Periodical cited type(5)

    1. 苏昕宇，梁志国，张宏扬，王海峰. 基于深度学习的联锁测试序列推荐方法. 铁道标准设计. 2024(09): 192-199 .
    2. 王霞，王恪铭，徐扬，唐伟健. 基于形式化方法的平交道口控制系统安全设计. 西南交通大学学报. 2023(01): 109-116 . 本站查看
    3. 袁飞军，王圣根，王亚飞. 基于信号集中监测系统的联锁试验. 铁道通信信号. 2023(02): 82-85 .
    4. 刘宁，韩程，王峥，侯锡立，王恪铭. 基于B方法的道岔控制系统形式化建模与验证. 铁路通信信号工程技术. 2022(06): 5-11 .
    5. 王若冲，韩笑，严紫薇. 基于UML模型的道岔控制安全逻辑分析及设计实现. 智慧轨道交通. 2022(05): 77-80 .

    Other cited types(8)

  • Created with Highcharts 5.0.7Amount of accessChart context menuAbstract Views, HTML Views, PDF Downloads StatisticsAbstract ViewsHTML ViewsPDF Downloads2024-052024-062024-072024-082024-092024-102024-112024-122025-012025-022025-032025-0405101520
    Created with Highcharts 5.0.7Chart context menuAccess Class DistributionFULLTEXT: 37.6 %FULLTEXT: 37.6 %META: 57.6 %META: 57.6 %PDF: 4.9 %PDF: 4.9 %FULLTEXTMETAPDF
    Created with Highcharts 5.0.7Chart context menuAccess Area Distribution其他: 12.0 %其他: 12.0 %Nepal: 0.2 %Nepal: 0.2 %上海: 0.6 %上海: 0.6 %东莞: 0.2 %东莞: 0.2 %临汾: 0.4 %临汾: 0.4 %保定: 0.2 %保定: 0.2 %北京: 6.7 %北京: 6.7 %哈尔滨: 0.2 %哈尔滨: 0.2 %哥伦布: 0.4 %哥伦布: 0.4 %唐山: 0.2 %唐山: 0.2 %嘉兴: 0.4 %嘉兴: 0.4 %四平: 0.2 %四平: 0.2 %天津: 0.6 %天津: 0.6 %孔敬: 0.4 %孔敬: 0.4 %宜春: 0.2 %宜春: 0.2 %广州: 0.4 %广州: 0.4 %张家口: 1.1 %张家口: 1.1 %成都: 7.5 %成都: 7.5 %扬州: 0.4 %扬州: 0.4 %昆明: 0.4 %昆明: 0.4 %杭州: 0.6 %杭州: 0.6 %格兰特县: 0.2 %格兰特县: 0.2 %桂林: 0.2 %桂林: 0.2 %武汉: 0.6 %武汉: 0.6 %池州: 0.6 %池州: 0.6 %泉州: 0.4 %泉州: 0.4 %洛阳: 0.2 %洛阳: 0.2 %深圳: 0.2 %深圳: 0.2 %温哥华: 0.2 %温哥华: 0.2 %温州: 0.2 %温州: 0.2 %漯河: 0.9 %漯河: 0.9 %盐城: 1.1 %盐城: 1.1 %石家庄: 0.7 %石家庄: 0.7 %芒廷维尤: 12.7 %芒廷维尤: 12.7 %芝加哥: 0.6 %芝加哥: 0.6 %苏州: 0.2 %苏州: 0.2 %衢州: 0.2 %衢州: 0.2 %西宁: 44.1 %西宁: 44.1 %西安: 0.2 %西安: 0.2 %西雅图: 0.4 %西雅图: 0.4 %贝伦: 0.2 %贝伦: 0.2 %贵阳: 0.2 %贵阳: 0.2 %运城: 1.1 %运城: 1.1 %郑州: 0.4 %郑州: 0.4 %重庆: 0.7 %重庆: 0.7 %长沙: 0.7 %长沙: 0.7 %其他Nepal上海东莞临汾保定北京哈尔滨哥伦布唐山嘉兴四平天津孔敬宜春广州张家口成都扬州昆明杭州格兰特县桂林武汉池州泉州洛阳深圳温哥华温州漯河盐城石家庄芒廷维尤芝加哥苏州衢州西宁西安西雅图贝伦贵阳运城郑州重庆长沙

Catalog

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

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

    1. 本站搜索
    2. 百度学术搜索
    3. 万方数据库搜索
    4. CNKI搜索

    Figures(7)  / Tables(4)

    Get Citation
    PDF
    XML
    Article views(555) PDF downloads(32) Cited by(13)
    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