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 条
  • [1] Formal Specification and Automated Verification of Railway Software with Frama-C
    Prevosto, Virgile
    Burghardt, Jochen
    Gerlach, Jens
    Hartig, Kerstin
    Pohl, Hans
    Voellinger, Kim
    2013 11TH IEEE INTERNATIONAL CONFERENCE ON INDUSTRIAL INFORMATICS (INDIN), 2013, : 710 - 715
  • [2] Formal Requirements Specification in Safety-critical Railway Signaling System
    Jo, Hyun-Jeong
    Hwang, Jong-Gyu
    Yoon, Yong-Ki
    T& D ASIA: 2009 TRANSMISSION & DISTRIBUTION CONFERENCE & EXPOSITION: ASIA AND PACIFIC, 2009, : 731 - 734
  • [3] Formal Verification of kLIBC with the WP Frama-C Plug-in
    Carvalho, Nuno
    Sousa, Cristiano da Silva
    Pinto, Jorge Sousa
    Tomb, Aaron
    NASA FORMAL METHODS, NFM 2014, 2014, 8430 : 343 - 358
  • [4] Formal Verification of a Java']JavaCard Virtual Machine with Frama-C
    Djoudi, Adel
    Hana, Martin
    Kosmatov, Nikolai
    FORMAL METHODS, FM 2021, 2021, 13047 : 427 - 444
  • [5] Formal Verification With Frama-C: A Case Study in the Space Software Domain
    Busquim e Silva, Rovedy Aparecida
    Arai, Nanci Naomi
    Burgareli, Luciana Akemi
    Parente de Oliveira, Jose Maria
    Pinto, Jorge Sousa
    IEEE TRANSACTIONS ON RELIABILITY, 2016, 65 (03) : 1163 - 1179
  • [6] FORMAL VERIFICATION OF SAFETY-CRITICAL SYSTEMS
    MOSER, LE
    MELLIARSMITH, PM
    SOFTWARE-PRACTICE & EXPERIENCE, 1990, 20 (08): : 799 - 821
  • [7] Verification of requirements for safety-critical software
    Carpenter, PB
    ACM SIGADA ANNUAL INTERNATIONAL CONFERENCE (SIGADA'99) - PROCEEDINGS, 1999, 19 (03): : 23 - 29
  • [8] Formal verification of safety-critical hybrid systems
    Livadas, C
    Lynch, NA
    HYBRID SYSTEMS: COMPUTATION AND CONTROL, 1998, 1386 : 253 - 272
  • [9] Formal Modeling and Verification of Safety-Critical Software
    Yoo, Junbeom
    Jee, Eunkyoung
    Cha, Sungdeok
    IEEE SOFTWARE, 2009, 26 (03) : 42 - 49
  • [10] Integrated formal verification of safety-critical software
    Ning Ge
    Eric Jenn
    Nicolas Breton
    Yoann Fonteneau
    International Journal on Software Tools for Technology Transfer, 2018, 20 : 423 - 440
12345