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 条
  • [21] Formal verification of fault tolerance in safety-critical reconfigurable modules
    Hammarberg J.
    Nadjm-Tehrani S.
    International Journal on Software Tools for Technology Transfer, 2005, 7 (3) : 268 - 279
  • [22] Security Requirements Engineering in Safety-Critical Railway Signalling Networks
    Heinrich, Markus
    Vateva-Gurova, Tsvetoslava
    Arul, Tolga
    Katzenbeisser, Stefan
    Suri, Neeraj
    Birkholz, Henk
    Fuchs, Andreas
    Krauss, Christoph
    Zhdanova, Maria
    Kuzhiyelil, Don
    Tverdyshev, Sergey
    Schlehuber, Christian
    SECURITY AND COMMUNICATION NETWORKS, 2019, 2019
  • [23] Formal specification as a tool for objective assessment of safety-critical interactive systems
    Palanque, P
    Bastide, R
    Paterno, F
    HUMAN-COMPUTER INTERACTION - INTERACT '97, 1997, : 323 - 330
  • [24] An effective technique for the software requirements analysis of NPP safety-critical systems, based on software inspection, requirements traceability, and formal specification
    Koo, SR
    Seong, PH
    Yoo, J
    Cha, SD
    Yoo, YJ
    RELIABILITY ENGINEERING & SYSTEM SAFETY, 2005, 89 (03) : 248 - 260
  • [25] Verification of Multiple Models of a Safety-Critical Motor Controller in Railway Systems
    Proenca, Jose
    Borrami, Sina
    de Nova, Jorge Sanchez
    Pereira, David
    Nandi, Giann Spilere
    RELIABILITY, SAFETY, AND SECURITY OF RAILWAY SYSTEMS: MODELLING, ANALYSIS, VERIFICATION, AND CERTIFICATION, RSSRAIL 2022, 2022, 13294 : 83 - 94
  • [26] Specifying Software Requirements for Safety-Critical Railway Systems: An Experience Report
    Provenzano, Luciana
    Hanninen, Kaj
    REQUIREMENTS ENGINEERING: FOUNDATION FOR SOFTWARE QUALITY, REFSQ 2017, 2017, 10153 : 363 - 369
  • [27] Formal Verification of an Industrial Safety-Critical Traffic Tunnel Control System
    Oortwijn, Wytse
    Huisman, Marieke
    INTEGRATED FORMAL METHODS, IFM 2019, 2019, 11918 : 418 - 436
  • [28] A Survey on Formal Verification Techniques for Safety-Critical Systems-on-Chip
    Grimm, Tomas
    Lettnin, Djones
    Huebner, Michael
    ELECTRONICS, 2018, 7 (06)
  • [29] A Design Flow with Integrated Verification of Requirements and Faults in Safety-Critical Systems
    Yan, Wei
    Fontaine, Daniel
    Chandy, John A.
    Michel, Laurent
    2017 12TH SYSTEM OF SYSTEMS ENGINEERING CONFERENCE (SOSE), 2017,
  • [30] An Approach for automated safety testing of safety-critical software system based on safety requirements
    Yu, Gang
    Xu, Zhong Wei
    Du, Jun Wei
    2009 INTERNATIONAL FORUM ON INFORMATION TECHNOLOGY AND APPLICATIONS, VOL 3, PROCEEDINGS, 2009, : 166 - 169
12345