• ISSN 0258-2724
  • CN 51-1277/U
  • EI Compendex
  • Scopus 收录
  • 全国中文核心期刊
  • 中国科技论文统计源期刊
  • 中国科学引文数据库来源期刊

车站联锁系统行为验证与数据确认的形式化方法

王恪铭 王霞 程鹏 刘宁 张传东

王恪铭, 王霞, 程鹏, 刘宁, 张传东. 车站联锁系统行为验证与数据确认的形式化方法[J]. 西南交通大学学报, 2021, 56(3): 587-593, 610. doi: 10.3969/j.issn.0258-2724.20191182
引用本文: 王恪铭, 王霞, 程鹏, 刘宁, 张传东. 车站联锁系统行为验证与数据确认的形式化方法[J]. 西南交通大学学报, 2021, 56(3): 587-593, 610. doi: 10.3969/j.issn.0258-2724.20191182
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
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

车站联锁系统行为验证与数据确认的形式化方法

doi: 10.3969/j.issn.0258-2724.20191182
基金项目: 国家自然科学基金(71502146,61673320);中央高校基本科研业务费专项资金(2682017ZT12)
详细信息
    作者简介:

    王恪铭(1981—),男,讲师,博士,研究方向为形式化建模与验证、运输系统优化,E-mail:kmwang@swjtu.edu.cn

  • 中图分类号: TP301.1; U284.3

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

  • 摘要: 车站联锁系统是一种典型的基于数据驱动的安全苛求系统,开发过程中需要对系统行为进行验证并需确认数据的正确性. 为此,通过分析联锁系统的设计规范,基于RODIN平台并使用Event-B语言,辅助使用UML (unified modeling language)图工具快速建立系统的初始模型,以自动生成模型文件并描述出各系统属性与事件流程;基于精化策略分层建模,对各层模型的证明义务进行定理证明,验证了系统的各项属性,得出可靠的通用功能模型;基于实例车站,对模型的公理进行了验证,同时实现了对联锁数据的确认;通过形式化验证过程,结合给定场景联锁数据的有效性确认,发现并纠正系统需求及分析过程中造成的潜在行为缺陷;通过功能仿真与验收测试,进一步确认了通用模型与联锁数据的正确性. 结果表明:本文方法提高了基于模型开发过程的准确性与层次性,验证了系统通用行为状态,且结合公理验证,实现了联锁数据的确认,并能基于模型进行功能场景仿真与测试,从而可进一步提高系统通用功能原型的可靠性.

     

  • 图 1  初始模型中事件的UML

    Figure 1.  UML diagram for event of initial model

    图 2  初始模型中的机器文件

    Figure 2.  Machine file in initial model

    图 3  精化模型一中train_into_route事件

    Figure 3.  Event of train_into_route in refined model 1

    图 4  数据确认的技术方案

    Figure 4.  Technical solution for data validation

    图 5  举例车站平面布置

    Figure 5.  Layout of an example railway station

    图 6  测试场景的步骤定义

    Figure 6.  Plain step definitions oftest scenario

    图 7  仿真测试举例

    Figure 7.  Example of simulation testing

    表  1  模型各层精化内容

    Table  1.   Refinement of the model

    精化层级引入对象
    第 1 层  建立列车对象,构造进路相关事件基本功能流程,如建立进路、进路正常解锁、进路取消、进路人工延时解锁和进路故障解锁等
    第 2 层  建立进路类型、进路方向、轨道区段类型、列车类型和敌对进路的定义,描述与进路、轨道区段、列车相关的功能与安全属性
    第 3 层  建立道岔对象,将道岔锁闭和解锁流程同步在建立进路和解锁进路事件中
    第 4 层  添加道岔的位置信息,增加道岔转动的计时约束,完善与道岔相关的事件
    第 5 层  建立信号机对象,完善人工延时解锁、取消进路等事件
    第 6 层  定义进路进程,增加信号设备故障和修复等事件,完善故障解锁流程
    下载: 导出CSV

    表  2  模型证明义务的证明情况统计

    Table  2.   Proving statistics of model proof obligations

    文件名称总数自动手动已修正未通过
    C0 1 1 0 0 0
    C1 6 5 1 0 0
    C2 4 2 2 0 0
    C3 2 2 0 0 0
    C4 6 6 0 0 0
    C5 5 3 2 0 0
    C6 0 0 0 0 0
    M0 0 0 0 0 0
    M1 80 49 31 0 0
    M2 59 17 42 0 0
    M3 46 17 29 0 0
    M4 118 41 77 0 0
    M5 146 61 85 0 0
    M6 237 218 19 0 0
    总计 710 422 288 0 0
    下载: 导出CSV

    表  3  举例车站联锁表

    Table  3.   Interlocking table of the example station

    方向进路信号机道岔轨道区段出站轨道区段敌对信号敌对进路迎面敌对进路编号
    名称显示
    发车进路股道 Ⅰ至 XSL1、31/3DGQ_1X17
    股道 Ⅱ至 XSL1、(3)1/3DGQ_1X28
    股道 Ⅲ至 XSL(1)、{3}1/3DGQ_1X39
    股道 Ⅰ至 SXL2、42/4DGQ_2S410
    股道 Ⅱ至 SXL(2)、{4}2/4DGQ_2S511
    股道 Ⅲ至 SXL2、(4)2/4DGQ_2S612
    注:信号机中,L表示绿灯;道岔中,1表示1# 道岔在定位,(1)表示1# 道岔在反位,{1}表示1# 道岔带动在定位,其余类推;轨道区段中,1/3DG表示1~3轨道区段,2/4DG表示2~4轨道区段.
    下载: 导出CSV

    表  4  公理验证结果

    Table  4.   Verification of axioms

    文件名称总数自动手动已修正未通过
    C073400
    C12271401
    C1_163300
    C21521300
    C393600
    C42016400
    C51401400
    C600000
    总计93345801
    下载: 导出CSV
  • 王恪铭,王峥. 基于形式化方法的道口控制系统规范建模与验证[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.
  • 加载中
图(7) / 表(4)
计量
  • 文章访问数:  503
  • HTML全文浏览量:  242
  • PDF下载量:  30
  • 被引次数: 0
出版历程
  • 收稿日期:  2019-12-16
  • 修回日期:  2020-06-08
  • 网络出版日期:  2020-08-24
  • 刊出日期:  2021-06-15

目录

    /

    返回文章
    返回