Functions and sizes of electronic control and software systems in automotives are being increased to achieve better controllability and reduce fuel consumption. A higher safety level is also demanded, so functional-safety standards are increasingly being introduced to in-vehicle systems.In safety critical systems, failure must be diagnosed and a system transited to a safe state when hardware failure occurs. Therefore, the failure diagnosis part of the basic software that takes charge of signal inputs and outputs processing must be verified for high accountability and explanations to a third party. To diagnose failure, the hardware and software that originally operate independently need to cooperate in principle. Hardware and software cooperating systems are not straight-forward to verify, because the combinations of conditions are too numerous for testing.The formal verification technology is effective, because it enables exhaustive verification of a vast quantity of test cases including unexpected states, such as a failed state. However, modeling methodology has not been established for timing related uncertainty between hardware failure and software.Our proposed method is to model a combination of the concurrent executions of both hardware and software operations under uncertain delay. We chose a C-language based model checker, which is formal verification software. We developed the uncertain delay injection mechanism and random hardware failure injection mechanism on the model checker software. Delay injection made it possible to model a concurrent hardware and software cooperating system with jitter and failure injection, which enables fail-safe behavior to be verified.


    Zugriff

    Zugriff prüfen

    Verfügbarkeit in meiner Bibliothek prüfen

    Bestellung bei Subito €


    Exportieren, teilen und zitieren



    Titel :

    Formal Verification Method for Safety Diagnosis Software


    Weitere Titelangaben:

    Sae Technical Papers


    Beteiligte:

    Kongress:

    SAE 2015 World Congress & Exhibition ; 2015



    Erscheinungsdatum :

    2015-04-14




    Medientyp :

    Aufsatz (Konferenz)


    Format :

    Print


    Sprache :

    Englisch




    Formal verification method for safety diagnosis software

    Narisawa,F. / Matsubara,M. / Nishi,M. et al. | Kraftfahrwesen | 2015


    Integrated Formal Verification and Validation of Safety Critical Software

    Ward, N. J. / North Atlantic Treaty Organization | British Library Conference Proceedings | 1993


    Formal Verification of Flight Critical Software

    Miller, Steven / Anderson, Elise / Wagner, Lucas et al. | AIAA | 2005


    Formal Verification of Safety-Critical Aerospace Systems

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