A formal approach for the construction and verification of railway control systems

被引：30
|
作者：
Haxthausen, Anne E. [1 ]
Peleska, Jan [2 ]
Kinder, Sebastian [2 ]
机构：
[1] Tech Univ Denmark, Dept Informat & Math Modelling, DK-2800 Lyngby, Denmark
[2] Univ Bremen, Dept Math & Comp Sci, Bremen, Germany
来源：
FORMAL ASPECTS OF COMPUTING | 2011年 / 23卷 / 02期
关键词：
Domain engineering; Domain-specific languages; Code generation; Formal methods; Verification; Railway control systems;
D O I：
10.1007/s00165-009-0143-6
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
This paper describes a complete model-based development and verification approach for railway control systems. For each control system to be generated, the user makes a description of the application-specific parameters in a domain-specific language. This description is automatically transformed into an executable control system model expressed in SystemC. This model is then compiled into object code. Verification is performed using three main methods applied to different levels. (0) The domain-specific description is validated wrt. internal consistency by static analysis. (1) The crucial safety properties are verified for the SystemC model by means of bounded model checking. (2) The object code is verified to be I/O behaviourally equivalent to the SystemC model from which it was compiled.
引用
收藏
页码：191 / 219
页数：29
相关论文
共 50 条
  • [1] A Formal Approach to Safety Verification of Railway Signaling Systems
    Russo, Aryldo G., Jr.
    Ladenberger, Lukas
    [J]. 2012 PROCEEDINGS - ANNUAL RELIABILITY AND MAINTAINABILITY SYMPOSIUM (RAMS), 2012,
  • [2] A Framework for Formal Verification and Validation of Railway Systems
    Benabbi, Yannis
    [J]. RIGOROUS STATE-BASED METHODS, ABZ 2023, 2023, 14010 : 371 - 374
  • [3] A domain-oriented, model-based approach for construction and verification of railway control systems
    Haxthausen, Anne E.
    Peleska, Jan
    [J]. FORMAL METHODS AND HYBRID REAL-TIME SYSTEMS, 2007, 4700 : 320 - +
  • [4] A Formal Approach for the Verification of Control Systems in Autonomous Driving Applications
    Skruch, Pawel
    Dlugosz, Marek
    Markiewicz, Pawel
    [J]. TRENDS IN ADVANCED INTELLIGENT CONTROL, OPTIMIZATION AND AUTOMATION, 2017, 577 : 178 - 189
  • [5] Verification of HMI safety for process control systems: a formal approach
    Lu, Shaowen
    Wu, Yongjian
    Yue, Heng
    [J]. 2011 9TH WORLD CONGRESS ON INTELLIGENT CONTROL AND AUTOMATION (WCICA 2011), 2011, : 188 - 191
  • [6] A formal approach for the specification, verification and control of flexible manufacturing systems
    Zairi, Sajeh
    Zouari, Belhassen
    Pitrac, Laurent
    [J]. ETFA 2007: 12TH IEEE INTERNATIONAL CONFERENCE ON EMERGING TECHNOLOGIES AND FACTORY AUTOMATION, VOLS 1-3, 2007, : 1031 - +
  • [7] Formal development and verification of a distributed railway control system
    Haxthausen, AE
    Peleska, J
    [J]. FM'99-FORMAL METHODS, VOL II, 1999, 1709 : 1546 - 1563
  • [8] Formal development and verification of a distributed railway control system
    Haxthausen, AE
    Peleska, J
    [J]. IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 2000, 26 (08) : 687 - 701
  • [9] Formal methods for railway control systems
    Alessandro Fantechi
    Francesco Flammini
    Stefania Gnesi
    [J]. International Journal on Software Tools for Technology Transfer, 2014, 16 : 643 - 646
  • [10] A Domain-Specific Framework for Automated Construction and Verification of Railway Control Systems
    Haxthausen, Anne E.
    [J]. COMPUTER SAFETY, RELIABILITY, AND SECURITY, PROCEEDINGS, 2009, 5775 : 1 - 3
12345