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.


    Zugriff

    Zugriff über TIB

    Verfügbarkeit in meiner Bibliothek prüfen

    Bestellung bei Subito €


    Exportieren, teilen und zitieren



    Titel :

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


    Weitere Titelangaben:

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


    Beteiligte:
    Hartig, Kerstin (Autor:in) / Gerlach, Jens (Autor:in) / Soto, Juan (Autor:in) / Busse, Jürgen (Autor:in)


    Erscheinungsdatum :

    2011


    Format / Umfang :

    9 Seiten, 3 Bilder, 1 Tabelle, 12 Quellen




    Medientyp :

    Aufsatz (Konferenz)


    Format :

    Print


    Sprache :

    Englisch




    Formal verification of safety requirements on complex systems

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


    Formal Verification of Safety-Critical Aerospace Systems

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


    Formal Verification of Safety Architectures for Automated Driving

    Eberhart, Clovis / Dubut, Jeremy / Haydon, James et al. | IEEE | 2023


    Deriving safety-critical system specification through requirements engineering

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