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

基于形式化方法的道口控制系统规范建模与验证

王恪铭 王峥

王恪铭, 王峥. 基于形式化方法的道口控制系统规范建模与验证[J]. 西南交通大学学报, 2019, 54(3): 573-578, 603. doi: 10.3969/j.issn.0258-2724.20180607
引用本文: 王恪铭, 王峥. 基于形式化方法的道口控制系统规范建模与验证[J]. 西南交通大学学报, 2019, 54(3): 573-578, 603. doi: 10.3969/j.issn.0258-2724.20180607
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
Citation: 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

基于形式化方法的道口控制系统规范建模与验证

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

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

  • 中图分类号: TP301.2;U213.8;U298.5

Modeling and Verification of Control System Specification for Railway Level Crossings Based on Formal Method

  • 摘要: 为了增强铁路道口控制系统设计的可靠性,使用一种形式化方法对该系统进行建模与验证. 基于道口管理规范,在分析系统各类属性与事件流程的基础上,使用UML图方法并结合精化策略建立了系统各层的Event-B语言模型. 通过对不变式的证明义务进行证明,验证了系统设计中的安全、时间特性,检查出了需求规范分析中的缺陷,提出了增强系统稳健性的改进方案,修正了系统的设计原型. 最后,通过不变式冲突与死锁检验进一步确认了模型的正确性. 研究表明文中方法提高了形式化建模过程的准确性与层次性,且确认得出目前规范中存在列车驶入道口时不能确保道口出清的缺陷,证实了使用本文形式化流程可以验证道口控制系统的需求规范并形成可靠的设计原型,从而可提高铁路道口的安全性.

     

  • 图 1  铁路道口控制系统示意

    Figure 1.  Schematic diagram of control system for railway level crossings

    图 2  道口控制系统中的事件流程

    Figure 2.  Events flows of control system for railway level crossings

    图 3  初始模型中的场景文件

    Figure 3.  Context file in the initial model

    图 4  初始模型中的UML图

    Figure 4.  UML diagram in the initial model

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

    Figure 5.  Machine file in the initial model

    图 6  基于特性的不变式验证

    Figure 6.  Property-based invariants verification

    图 7  添加事件的防卫条件

    Figure 7.  Additional guards of event

    图 8  精化过程中的证明义务统计

    Figure 8.  Statistics of proof obligation in the refinement processes

    图 9  道口异常处理流程

    Figure 9.  Exception-handling process of the railway level crossings

    图 10  新增对应的异常处理流程不变式验证

    Figure 10.  Additional invariants verification of exception-handling process

    表  1  模型精化过程

    Table  1.   Refinement processes of the model

    精化层级引入对象
    第1层引入栏门、控制器对象,建立栏门开启与关闭的过程事件.
    第2层引入时间对象,建立系统时钟,完善栏门接收控制器命令后开启与关闭过程的时间要求.
    第3层引入列车、信号灯对象,增加列车接近、列车逼近、列车离去道口事件与信号灯转换事件,完善道口系统执行过程.
    第4层引入列车接近、逼近计时,完善控制器的时间约束.
    下载: 导出CSV
  • 国家安全生产监管管理总局. 铁路运输行业基本情况[R/OL]. (2014-06-17)[2018-01-04]. http://www.chinasafety.gov.cn/newpage/Contents/Channel_21500/2014/0617/236238/content_236238.htm
    European Union Agency for Railways. Railway safety performance in the european union[R/OL]. (2016-09-13)[2018-01-04]. http://www.era.europa.eu/Document-Register/Documents/Railway%20Safety%20Performance%202016%20final%20E.pdf
    Eurostat. Rail accident fatalities in the EU[R/OL]. (2017-02-10)[2018-01-04]. http://ec.europa.eu/eurostat/statistics-explained/index.php/Rail_accident_fatalities_in_the_EU#Further_Eurostat_information
    贾明涛,王海星,肖贵平. 铁路道口安全影响因素分析及对策[J]. 安全与环境学报,2006,6(6): 123-126. doi: 10.3969/j.issn.1009-6094.2006.06.033

    JIA Mingtao, WANG Haixing, XIAO Guiping. Safety analysis on highway-railway crossings[J]. Journal of Safety and Environment, 2006, 6(6): 123-126. doi: 10.3969/j.issn.1009-6094.2006.06.033
    GHAZEL M, EL-KOURSI E M. Two-half-barrier level crossings versus four-half-barrier level crossings:a comparative risk analysis study[J]. IEEE Transactions on Intelligent Transportation Systems, 2014, 15(3): 1123-1133. doi: 10.1109/TITS.2013.2294874
    MEKKI A, GHAZEL M, TOGUYENI A. Validation of a new functional design of automatic protection systems at level crossings with model-checking techniques[J]. IEEE Transactions on Intelligent Transportation Systems, 2012, 13(2): 714-723. doi: 10.1109/TITS.2011.2178238
    SALMANE H, KHOUDOUR L, RUICHEK Y. A video-analysis-based railway-road safety system for detecting Hazard situations at level crossings[J]. IEEE Transactions on Intelligent Transportation Systems, 2015, 16(2): 596-609.
    LARSEN P G, LARSEN P G, BICARREGUI J, et al. Formal methods:practice and experience[J]. ACM Computing Surveys, 2009, 41(4): 1-40.
    CENELEC. IEC61508: Functional safety of electrical/electronic/programmable electronic safety-reared systems[S/OL]. European Committee for Electrotechnical Standardization. [2018-01-04]. https://webstore.iec.ch/preview/info_iec61508-0%7Bed1.0%7Db.pdf
    SUN J, SUN S, LI K, et al. Efficient algorithm for traffic engineering in cloud-of-things and edge computing[J]. Computers & Electrical Engineering, 2018, 69(7): 610-627.
    LEFFINGWELL D, WIDRIG D. Managing software requirements: a use case approach[M]. New Jersey: Addison-Wesley, 2003: 10-40
    国家铁路局. 铁路站内道口信号设备技术条件: GB10493—2018[S]. 北京: 中国标准出版社, 2018: 3-5
    中国铁路总公司. 铁路道口管理办法: 铁总运[2013]121号[S/OL]. 北京: [s.n.], 2013: 10-19. [2018-01-04]. https://wenku.baidu.com/view/fe0322d649649b6648d74789.html
    ABRIAL J R. Modeling in Event-B: system and software engineering[M]. Cambridge: Cambridge University Press, 2010: 217-219
    BUTLER M. Reasoned modelling with Event-B[C]//Engineering Trustworthy Software Systems, SETSS 2016. Cham: Springer, 2016: 51-109
    WANG K. Rail level crossing DATA[CP/OL]. [2018-5-21]. https://github.com/abidefei/RailLevelCrossing_EventB
    ZHU C, BUTLER M, CIRSTEA C. Refinement of timing constraints for concurrent tasks with scheduling[C]//International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z. Cham: Springer, 2018: 219-233
  • 加载中
图(10) / 表(1)
计量
  • 文章访问数:  437
  • HTML全文浏览量:  205
  • PDF下载量:  13
  • 被引次数: 0
出版历程
  • 收稿日期:  2018-07-16
  • 修回日期:  2018-09-18
  • 网络出版日期:  2019-03-30
  • 刊出日期:  2019-06-01

目录

    /

    返回文章
    返回