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 条
  • [31] Scenario driven requirements specification of safety-critical real-time systems
    Lin, JJ
    Kung, DC
    Hsia, P
    COMPUTERS AND THEIR APPLICATIONS - PROCEEDINGS OF THE ISCA 11TH INTERNATIONAL CONFERENCE, 1996, : 284 - 287
  • [32] Verification of a safety-critical railway interlocking system with real-time constraints
    Hartonas-Garmhausen, V
    Campos, S
    Cimatti, A
    Clarke, E
    Giunchiglia, F
    TWENTY-EIGHTH ANNUAL INTERNATIONAL SYMPOSIUM ON FAULT-TOLERANT COMPUTING, DIGEST PAPERS, 1998, : 458 - 463
  • [33] Verification of a safety-critical railway interlocking system with real-time constraints
    Hartonas-Garmhausen, V
    Campos, S
    Cimatti, A
    Clarke, E
    Giunchiglia, F
    SCIENCE OF COMPUTER PROGRAMMING, 2000, 36 (01) : 53 - 64
  • [34] Natural Language Processing based Auto Generation of Proof Obligations for Formal Verification of Control Requirements in Safety-Critical Systems
    Shivamurthy, Jagadish
    Vidyarthi, Deepti
    Uppal, Tarun
    IFAC PAPERSONLINE, 2024, 57 : 1 - 6
  • [35] LaQuSo: Using Formal Methods for Analysis, Verification and Improvement of Safety-Critical Software
    Smetsers, Sjaak
    van Eekelen, Marko
    ERCIM NEWS, 2008, (75): : 36 - 37
  • [36] Development of a normative package for safety-critical software using formal regulatory requirements
    Vilkomir, SA
    Ghose, AK
    PRODUCT FOCUSED SOFTWARE PROCESS IMPROVEMENT, 2004, 3009 : 523 - 537
  • [37] From Rigorous Requirements Engineering to Formal System Design of Safety-Critical Systems
    Ponsard, Christophe
    Massonet, Philippe
    Dallons, Gautier
    ERCIM NEWS, 2008, (75): : 22 - 23
  • [38] Formal verification and validation of a movement control actor relocation algorithm for safety-critical applications
    Imran, Muhammad
    Zafar, Nazir Ahmad
    Alnuem, Mohammed Abdullah
    Aksoy, Mehmet Sabih
    Vasilakos, Athanasios V.
    WIRELESS NETWORKS, 2016, 22 (01) : 247 - 265
  • [39] Hierarchical safety analysis and formal verification for safety-critical systems using STAMP and Event-B
    Chen, Zuxi
    Niu, Chuanjun
    Mei, Meng
    Zhang, Hongyang
    SAFETY SCIENCE, 2025, 184
  • [40] A Component-Based Approach for the Specification and Verification of Safety-Critical Software: Application to a Platoon of Vehicles
    Souquieres, Jeanine
    ERCIM NEWS, 2008, (75): : 33 - 34
12345