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 条
  • [21] Industrialising a proof-based verification approach of computerised interlocking systems
    Behnia, S.
    Mammar, A.
    Mota, J-M.
    Breton, N.
    Caspi, P.
    Raymond, P.
    COMPUTERS IN RAILWAYS XI: COMPUTER SYSTEM DESIGN AND OPERATION IN THE RAILWAY AND OTHER TRANSIT SYSTEMS, 2008, 103 : 143 - 152
  • [22] An automatic formal model generation and verification method for railway interlocking systems
    Oz, Muhammed Ali
    Kaymakci, Ozgur Turay
    Gazi University Journal of Science, 2017, 30 (02): : 133 - 147
  • [23] A Knowledge Based Solution for Intelligent Verification and Validation of Interlocking Railway Systems
    Bellini, Pierfrancesco
    Nesi, Paolo
    Zaza, Imad
    ERCIM NEWS, 2015, (103): : 36 - 37
  • [24] Modelling, Simulation and Code Generation for Electronic Railway Interlocking Systems
    Ghignone, Ramiro
    Falco, Cristian
    Larosa, Facundo
    Mendes, Heman
    Chang, Leandro
    Menendez, Martin
    Lutenberg, Ariel
    IEEE LATIN AMERICA TRANSACTIONS, 2021, 19 (01) : 155 - 162
  • [25] A toolset for modelling and verification of GALS systems
    Ramesh, S
    Sonalkar, S
    D'silva, V
    Chandra, N
    Vijayalakshmi, B
    COMPUTER AIDED VERIFICATION, 2004, 3114 : 506 - 509
  • [26] Hierarchical modelling of complex control systems: dependability analysis of a railway interlocking
    Bondavalli, A
    Nelli, M
    Simoncini, L
    Mongardi, G
    COMPUTER SYSTEMS SCIENCE AND ENGINEERING, 2001, 16 (04): : 249 - 261
  • [27] RELAY INTERLOCKING PLANT OF DANISH STATE RAILWAYS
    HANSEN, WW
    ERICSSON REVIEW, 1968, 45 (03): : 112 - &
  • [28] Interlocking Formal Verification at Alstom Signalling
    Parillaud, Camille
    Fonteneau, Yoann
    Belmonte, Fabien
    RELIABILITY, SAFETY, AND SECURITY OF RAILWAY SYSTEMS: MODELLING, ANALYSIS, VERIFICATION, AND CERTIFICATION, 2019, 11495 : 215 - 225
  • [29] Safety Invariant Engineering for Interlocking Verification
    Iliasov, Alexei
    Taylor, Dominic
    Laibinis, Linas
    Romanovsky, Alexander
    COMPUTER SAFETY, RELIABILITY, AND SECURITY, SAFECOMP 2024, 2024, 14988 : 68 - 83
  • [30] Verification of Solid State Interlocking Programs
    James, Phillip
    Lawrence, Andy
    Moller, Faron
    Roggenbach, Markus
    Seisenberger, Monika
    Setzer, Anton
    Kanso, Karim
    Chadwick, Simon
    SOFTWARE ENGINEERING AND FORMAL METHODS, 2014, 8368 : 253 - 268
12345