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 条
  • [1] Towards a Framework for Modelling and Verification of Relay Interlocking Systems
    Haxthausen, Anne E.
    FOUNDATIONS OF COMPUTER SOFTWARE: MODELING, DEVELOPMENT, AND VERIFICATION OF ADAPTIVE SYSTEMS, 2011, 6662 : 176 - 192
  • [2] CSP Specification and Verification of Relay-based Railway Interlocking Systems
    Pereira, D. I. de Almeida
    Oliveira, M. V. M.
    Bezerra, P. E. R.
    Bon, P.
    Collart-Dutilleul, S.
    37TH ANNUAL ACM SYMPOSIUM ON APPLIED COMPUTING, 2022, : 97 - 106
  • [3] Formal modelling and verification of interlocking systems featuring sequential release
    Linh Hong Vu
    Haxthausen, Anne E.
    Peleska, Jan
    SCIENCE OF COMPUTER PROGRAMMING, 2017, 133 : 91 - 115
  • [4] Decomposing the Verification of Interlocking Systems
    Haxthausen, Anne E.
    Fantechi, Alessandro
    Gori, Gloria
    Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2023, 14165 LNCS : 96 - 113
  • [5] Verification of railway interlocking systems
    Busard, Simon
    Cappart, Quentin
    Limbree, Christophe
    Pecheur, Charles
    Schaus, Pierre
    ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2015, (184): : 19 - 31
  • [6] Compositional Verification of Railway Interlocking Systems
    Haxthausen, Anne Elisabeth
    Fantechi, Alessandro
    FORMAL ASPECTS OF COMPUTING, 2023, 35 (01)
  • [7] Automated Compositional Verification of Interlocking Systems
    Haxthausen, Anne E.
    Fantechi, Alessandro
    Gori, Gloria
    Mikkelsen, Oli Karason
    Petersen, Sofie-Amalie
    RELIABILITY, SAFETY, AND SECURITY OF RAILWAY SYSTEMS, RSSRAIL 2023, 2023, 14198 : 146 - 164
  • [8] CSP Specification and Verification of a Relay-Based Railway Interlocking System
    Bezerra, P. E. R.
    Oliveira, M. V. M.
    Lecomte, Thierry
    de Almeida Pereira, D. I.
    FORMAL METHODS: FOUNDATIONS AND APPLICATIONS, SBMF 2023, 2024, 14414 : 36 - 54
  • [9] On the Use of Static Checking in the Verification of Interlocking Systems
    Haxthausen, Anne E.
    Ostergaard, Peter H.
    LEVERAGING APPLICATIONS OF FORMAL METHODS, VERIFICATION AND VALIDATION: DISCUSSION, DISSEMINATION, APPLICATIONS, ISOLA 2016, PT II, 2016, 9953 : 266 - 278
  • [10] Comparing Formal Verification Approaches of Interlocking Systems
    Haxthausen, Anne Elisabeth
    Hoang Nga Nguyen
    Roggenbach, Markus
    RELIABILITY, SAFETY, AND SECURITY OF RAILWAY SYSTEMS: MODELLING, ANALYSIS, VERIFICATION, AND CERTIFICATION, RSSRAIL 2016, 2016, 9707 : 160 - 177
12345