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 条
  • [41] Modelling and Verification of Real-Time Systems with Alvis
    Szpyrka, Marcin
    Podolski, Lukasz
    Wypych, Michal
    TOWARDS A SYNERGISTIC COMBINATION OF RESEARCH AND PRACTICE IN SOFTWARE ENGINEERING, 2018, 733 : 165 - 178
  • [42] Kernel P systems: From modelling to verification and testing
    Gheorghe, Marian
    Ceterchi, Rodica
    Ipate, Florentin
    Konur, Savas
    Lefticaru, Raluca
    THEORETICAL COMPUTER SCIENCE, 2018, 724 : 45 - 60
  • [43] A Compositional Modelling and Verification Framework for Stochastic Hybrid Systems
    Wang, Shuling
    Zhan, Naijun
    Zhang, Lijun
    FORMAL ASPECTS OF COMPUTING, 2017, 29 (04) : 751 - 775
  • [44] Efficient Modelling of Embedded Software Systems and Their Formal Verification
    Estivill-Castro, Vladimir
    Hexel, Rene
    Rosenblueth, David A.
    2012 19TH ASIA-PACIFIC SOFTWARE ENGINEERING CONFERENCE (APSEC), VOL 1, 2012, : 428 - 433
  • [45] MODELLING, SIMULATION AND VERIFICATION OF PNEUMATICALLY ACTUATED AUXETIC SYSTEMS
    Theodoros, Themistocleous
    PROCEEDINGS OF THE 18TH INTERNATIONAL CONFERENCE ON COMPUTER-AIDED ARCHITECTURAL DESIGN RESEARCH IN ASIA (CAADRIA 2013): OPEN SYSTEMS, 2013, : 395 - 404
  • [46] Fault diagnosis for discrete event systems: Modelling and verification
    Simeu-Abazi, Zineb
    Di Mascolo, Maria
    Knotek, Michal
    RELIABILITY ENGINEERING & SYSTEM SAFETY, 2010, 95 (04) : 369 - 378
  • [47] Model Checking-based Safety Verification of a Petri Net Representation of Train Interlocking Systems
    Aristyo, B.
    Pradityo, K.
    Tamba, T. A.
    Nazaruddin, Y. Y.
    Widyotriatmo, A.
    2018 57TH ANNUAL CONFERENCE OF THE SOCIETY OF INSTRUMENT AND CONTROL ENGINEERS OF JAPAN (SICE), 2018, : 392 - 397
  • [48] Modelling and Verification of Safety of Access Control in SCADA Systems
    Vistbakka, Inna
    Troubitsyna, Elena
    RISKS AND SECURITY OF INTERNET AND SYSTEMS (CRISIS 2020), 2021, 12528 : 354 - 364
  • [49] Formal Virtual Modelling and Data Verification for Supervision Systems
    Lecomte, Thierry
    FM 2015: FORMAL METHODS, 2015, 9109 : 597 - 600
  • [50] Modelling and verification of reconfigurable multi-agent systems
    Yehia Abd Alrahman
    Nir Piterman
    Autonomous Agents and Multi-Agent Systems, 2021, 35
12345