Modelling and Verification of Relay Interlocking Systems

被引：0
|
作者：
Haxthausen, Anne E. [1 ]
Le Bliguet, Marie [1 ]
Kjaer, Andreas A. [1 ]
机构：
[1] Tech Univ Denmark, Dept Informat & Math Modelling, DTU Informat, DK-2800 Lyngby, Denmark
来源：
FOUNDATIONS OF COMPUTER SOFTWARE: FUTURE TRENDS AND TECHNIQUES FOR DEVELOPMENT | 2010年 / 6028卷
关键词：
D O I：
暂无
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
This paper describes how relay interlocking systems as used by the Danish railways can be formally modelled and verified. Such systems are documented by circuit diagrams describing their static layout. It is explained how to derive a state transition system model for the dynamic behaviour of a relay system from such diagrams. Safety properties are identified and formalised as LTL formulae. Model checking is finally used to verify that a model satisfies the safety properties. The method is tested for an existing station in Denmark.
引用
收藏
页码：141 / 153
页数：13
相关论文
共 50 条
  • [31] Formal Methods for Industrial Interlocking Verification
    Chadwick, Simon
    James, Phillip
    Roggenbach, Markus
    Werner, Tom
    2018 INTERNATIONAL CONFERENCE ON INTELLIGENT RAIL TRANSPORTATION (ICIRT), 2018,
  • [32] Relay based modelling of cascaded systems with propagation delay
    Pandey, Saurabh
    IFAC PAPERSONLINE, 2024, 57 : 415 - 420
  • [33] Formal Modelling and Verification of Concurrent Systems with XCCS
    Szpyrka, Marcin
    Matyasik, Piotr
    PROCEEDINGS OF THE INTERNATIONAL SYMPOSIUM ON PARALLEL AND DISTRIBUTED COMPUTING, 2008, : 454 - 458
  • [34] Modelling and Verification of Survivability Requirements for Critical Systems
    Bernardi, Simona
    Dranca, Lacramioara
    Merseguer, Jose
    SOFTWARE ENGINEERING AND FORMAL METHODS, SEFM 2014, 2015, 8938 : 86 - 100
  • [35] Robot Swarms as Hybrid Systems: Modelling and Verification
    Schupp, Stefan
    Leofante, Francesco
    Behr, Leander
    Abraham, Erika
    Taccella, Armando
    ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2021, (361): : 61 - 77
  • [36] Modelling and verification of weighted spiking neural systems
    Aman, Bogdan
    Ciobanu, Gabriel
    THEORETICAL COMPUTER SCIENCE, 2016, 623 : 92 - 102
  • [37] An approach to modelling and verification of component based systems
    Gossler, Gregor
    Graf, Sussane
    Majster-Cederbaum, Mila
    Martens, M.
    Sifakis, Joseph
    SOFSEM 2007: THEORY AND PRACTICE OF COMPUTER SCIENCE, PROCEEDINGS, 2007, 4362 : 295 - +
  • [38] Verification of Railway Interlocking - Compositional Approach with OCRA
    Limbree, Christophe
    Cappart, Quentin
    Pecheur, Charles
    Tonetta, Stefano
    RELIABILITY, SAFETY, AND SECURITY OF RAILWAY SYSTEMS: MODELLING, ANALYSIS, VERIFICATION, AND CERTIFICATION, RSSRAIL 2016, 2016, 9707 : 134 - 149
  • [39] Distributed interlocking system and its safety verification
    Hei, Xinhong
    Takahashi, Sei
    Nakamura, Hideo
    WCICA 2006: SIXTH WORLD CONGRESS ON INTELLIGENT CONTROL AND AUTOMATION, VOLS 1-12, CONFERENCE PROCEEDINGS, 2006, : 8612 - +
  • [40] Friction modelling of servomechanical systems with dual-relay feedback
    Chen, S. L.
    Tan, K. K.
    Huang, S. N.
    IECON 2007: 33RD ANNUAL CONFERENCE OF THE IEEE INDUSTRIAL ELECTRONICS SOCIETY, VOLS 1-3, CONFERENCE PROCEEDINGS, 2007, : 557 - 562
12345