Formal Specification and Automated Verification of Safety-Critical Requirements of a Railway Vehicle with Frama-C/Jessie

被引：4
|
作者：
Hartig, Kerstin [1 ]
Gerlach, Jens [1 ]
Soto, Juan [1 ]
Busse, Juergen [2 ]
机构：
[1] Fraunhofer FIRST, Berlin, Germany
[2] IfB GmbH, Inst Railway Technol, Berlin, Germany
来源：
FORMS/FORMAT 2010: FORMAL METHODS FOR AUTOMATION AND SAFETY IN RAILWAY AND AUTOMOTIVE SYSTEMS | 2011年
关键词：
Frama-C/Jessie; ACSL; Unit Proof; EN; 50128; Railway Domain;
D O I：
10.1007/978-3-642-14261-1_15
中图分类号：
U [交通运输];
学科分类号：
08 ; 0823 ;
摘要：
Formal verification of software provides a higher level of assurance than classical software testing. In this paper, we report on our experience with the Frama-C/Jessie verification tool in the railway domain. We analyse safety-critical requirements of a railway vehicle, formalize them using the ANSI/ISO-C Specification Language (ACSL) and achieve automated proofs to verify that the implementation satisfies the formal specification. The main requirement for the successful application of Frama-C in the railway domain is its qualification according to EN 50128.
引用
收藏
页码：145 / 153
页数：9
相关论文
共 50 条
  • [41] Optimization Techniques and Formal Verification for the Software Design of Boolean Algebra Based Safety-Critical Systems
    Perez, Jon
    Flores, Jose Luis
    Blum, Christian
    Cerquides, Jesus
    Abuin, Alex
    IEEE TRANSACTIONS ON INDUSTRIAL INFORMATICS, 2022, 18 (01) : 620 - 630
  • [42] From the specification of multiagent systems by statecharts to their formal analysis by model checking: Towards safety-critical applications
    Stolzenburg, F
    Arai, T
    MULTIAGENT SYSTEM TECHNOLOGIES, PROCEEDINGS, 2003, 2831 : 131 - 143
  • [43] On design and formal verification of SNSP: a novel real-time communication protocol for safety-critical applications
    Zhou, Rui
    Li, Chanjuan
    Min, Rong
    Yu, Qi
    Gu, Fei
    Zhou, Qingguo
    Hung, Jason C.
    Li, Kuan-Ching
    Wang, Xuan
    JOURNAL OF SUPERCOMPUTING, 2014, 69 (03): : 1254 - 1283
  • [44] On design and formal verification of SNSP: a novel real-time communication protocol for safety-critical applications
    Rui Zhou
    Chanjuan Li
    Rong Min
    Qi Yu
    Fei Gu
    Qingguo Zhou
    Jason C. Hung
    Kuan-Ching Li
    Xuan Wang
    The Journal of Supercomputing, 2014, 69 : 1254 - 1283
  • [45] Asynchronous Programming with Futures in C on a Safety-Critical Platform in the Railway-Control Domain
    Duarte, Oscar Medina
    Hametner, Reinhard
    2017 22ND IEEE INTERNATIONAL CONFERENCE ON EMERGING TECHNOLOGIES AND FACTORY AUTOMATION (ETFA), 2017,
  • [46] Deductive Functional Verification of Safety-Critical Embedded C-Code: An Experience Report
    Gurov, Dilian
    Lidstrom, Christian
    Nyberg, Mattias
    Westman, Jonas
    CRITICAL SYSTEMS: FORMAL METHODS AND AUTOMATED VERIFICATION (FMICS-AVOCS 2017), 2017, 10471 : 3 - 18
  • [47] Aiding Modular Design and Verification of Safety-Critical Time-Triggered Systems by Use of Executable Formal Specifications
    Sakurai, Kohei
    Bokor, Peter
    Suri, Neeraj
    11TH IEEE HIGH ASSURANCE SYSTEMS ENGINEERING SYMPOSIUM, PROCEEDINGS, 2008, : 261 - 270
  • [48] Verification of a Real-Time Safety-Critical Protocol Using a Modelling Language with Formal Data and Behaviour Semantics
    Toth, Tamas
    Voeroes, Andras
    Majzik, Istvan
    COMPUTER SAFETY, RELIABILITY, AND SECURITY, 2014, 8696 : 207 - 218
  • [49] Formal Verification of a Dependable State Machine-Based Hardware Architecture for Safety-Critical Cyber-Physical Systems: Analysis, Design, and Implementation
    Khairullah, Shawkat Sabah
    JOURNAL OF ELECTRONIC TESTING-THEORY AND APPLICATIONS, 2024, 40 (04): : 509 - 523
  • [50] C2AADL_Reverse: A model-driven reverse engineering approach to development and verification of safety-critical software
    Yang, Zhibin
    Qiu, Zhikai
    Zhou, Yong
    Huang, Zhiqiu
    Bodeveix, Jean-Paul
    Filali, Mamoun
    JOURNAL OF SYSTEMS ARCHITECTURE, 2021, 118
12345