Formal Methods for Industrial Interlocking Verification

被引:0
|
作者
Chadwick, Simon [1 ]
James, Phillip [2 ]
Roggenbach, Markus [2 ]
Werner, Tom [1 ]
机构
[1] Siemens Rail Automat UK, Chippenham, England
[2] Swansea Univ, Comp Sci, Swansea, W Glam, Wales
关键词
Verification; Model-Checking; PLC; Formal Methods in Industry;
D O I
暂无
中图分类号
TM [电工技术]; TN [电子技术、通信技术];
学科分类号
0808 ; 0809 ;
摘要
In this paper, we present an overview of research jointly undertaken by the Swansea Railway Verification Group towards verification techniques for automatically checking safety for train control systems. We present a comprehensive modelling of safety principles in first order logic. We conclude by applying verification methods developed by Swansea Railway Verification Group in order to check the modelled safety principles against a real world railway interlocking system.
引用
收藏
页数:5
相关论文
共 50 条
  • [1] Interlocking Formal Verification at Alstom Signalling
    Parillaud, Camille
    Fonteneau, Yoann
    Belmonte, Fabien
    [J]. RELIABILITY, SAFETY, AND SECURITY OF RAILWAY SYSTEMS: MODELLING, ANALYSIS, VERIFICATION, AND CERTIFICATION, 2019, 11495 : 215 - 225
  • [2] Comparing Formal Verification Approaches of Interlocking Systems
    Haxthausen, Anne Elisabeth
    Hoang Nga Nguyen
    Roggenbach, Markus
    [J]. RELIABILITY, SAFETY, AND SECURITY OF RAILWAY SYSTEMS: MODELLING, ANALYSIS, VERIFICATION, AND CERTIFICATION, RSSRAIL 2016, 2016, 9707 : 160 - 177
  • [3] Industrial experience with formal verification
    Payer, Michael
    [J]. IT - Information Technology, 2001, 43 (01): : 16 - 21
  • [4] Formal Modelling and Verification of an Interlocking Using mCRL2
    Bouwman, Mark
    Janssen, Bob
    Luttik, Bas
    [J]. FORMAL METHODS FOR INDUSTRIAL CRITICAL SYSTEMS, FMICS 2019, 2019, 11687 : 22 - 39
  • [5] Formal Modeling and Verification of Interlocking Systems Featuring Sequential Release
    Vu, Linh H.
    Haxthausen, Anne E.
    Peleska, Jan
    [J]. FORMAL TECHNIQUES FOR SAFETY-CRITICAL SYSTEMS, FTSCS 2014, 2015, 476 : 223 - 238
  • [6] Case study: Formal specification and verification of railway interlocking system
    Hlavaty, T
    Preucil, L
    Stepan, P
    [J]. PROCEEDINGS OF THE 27TH EUROMICRO CONFERENCE - 2001: A NET ODYSSEY, 2001, : 258 - 263
  • [7] Validation of Railway Interlocking Systems by Formal Verification, A Case Study
    Bonacchi, Andrea
    Fantechi, Alessandro
    Bacherini, Stefano
    Tempestini, Matteo
    Cipriani, Leonardo
    [J]. SOFTWARE ENGINEERING AND FORMAL METHODS, 2014, 8368 : 237 - 252
  • [8] Formal modelling and verification of interlocking systems featuring sequential release
    Linh Hong Vu
    Haxthausen, Anne E.
    Peleska, Jan
    [J]. SCIENCE OF COMPUTER PROGRAMMING, 2017, 133 : 91 - 115
  • [9] Applying formal verification to the AAMP5 microprocessor: A case study in the industrial use of formal methods
    Srivas, MK
    Miller, SP
    [J]. FORMAL METHODS IN SYSTEM DESIGN, 1996, 8 (02) : 153 - 188
  • [10] Challenges for formal verification in industrial setting
    Slobodova, Anna
    [J]. FORMAL METHODS: APPLICATIONS AND TECHNOLOGY, 2007, 4346 : 1 - 22