Formal verification of software provides a higher level of assurance than classical software testing. It is reported on our experience with the Frama-C/Jessie verification tool in the railway domain. It are analysed 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. It are demonstrated an approach and a procedure for verifying safety critical software components in an automated way. In our experience, an ACSL specification can form a crucial artifact for communicating within the development process because many participants in this process can relate to ACSL, e.g., requirements engineers, architects, software developers or assessors. Regarding the scalability of the approach, it is thought that the main focus of deductive verification will be on relatively small, well understood software components and on software subsystems that consist of such components. However, even so the return on investment of deductive verification compared to traditional component testing is not yet well understood and will be part of our future research. Nevertheless, there are still challenges to manage. First of all, formal specification and deductive verification need to be properly integrated in the software development process. This is of utmost importance for high-integrity applications where authorities must be convinced to accept replacing unit tests by unit proofs. In order to use deductive verification efficiently, advanced user knowledge is expected. Software developers must be trained in the art of writing annotations and in the use of Frama-C tools. If a proof cannot be accomplished it may be non-trivial to determine the source of the problem. Better feedback (recommendations) must be provided by the tool to aid in troubleshooting. Safety-critical software in the railway domain must be assessed before it is placed into service. The assessment process is described in the European standard EN 50128:2001. From the assessors point of view, the main requirement for deductive verification methodology and tools is their qualification. Qualification in that context means a particular trustworthiness. That trustworthiness must be proven and documented. The EN 50128 standard does not address verification tools directly. Requirements in the field are in evolution. To summarize, the main requirements are documentation of the tools behavior and of any constraints in its use, combined with successful validation of the tool. The safety argument for the tool, has to address, that faults within the source code must not be proven. One approach to reach that goal is undertaking test suites on source code with intentionally intruded faults.


    Access

    Access via TIB

    Check availability in my library

    Order at Subito €


    Export, share and cite



    Title :

    Formal specification and automated verification of safety-critical requirements of a railway vehicle with Frama-C/Jessie


    Additional title:

    Formale Spezifikation und automatische Verifikation sicherheitskritischer Forderungen eines Eisenbahnfahrzeugs mittels Frama-C/Jessie


    Contributors:


    Publication date :

    2011


    Size :

    9 Seiten, 3 Bilder, 1 Tabelle, 12 Quellen




    Type of media :

    Conference paper


    Type of material :

    Print


    Language :

    English




    Formal Specification of Railway Control Systems

    Xu, Bingqing / Zhang, Lichen | Springer Verlag | 2013


    Formal verification of safety requirements on complex systems

    Bernardeschi, C. / Fantechi, A. / Gnesi, S. | Tema Archive | 1996


    Formal Verification of Safety-Critical Aerospace Systems

    Paul, Saswata / Cruz, Elkin / Dutta, Airin et al. | IEEE | 2023


    Deriving safety-critical system specification through requirements engineering

    Fukuda, Mitsuyoshi / Hirao, Yuji / Tsuchiya, Ryuji | IuD Bahn | 1998


    Formal Verification of Intersection Safety for Automated Driving

    Haydon, James / Bondu, Martin / Eberhart, Clovis et al. | IEEE | 2023