Formal verification is increasingly used for checking and proving the correctness of digital systems. In this paper, we present formal verification as a cost-effective technique for the verification and validation of model-based safety-critical embedded systems.We start by explaining how formal verification can be easily integrated in a model-based development methodology for critical embedded software. In the methodology examined, the development methods are based upon a formal and deterministic language representation and a correct-by-construction automatic code generation. In this methodology, formal verification proves that what you execute conforms to safety requirements, and what you execute is exactly what you embed. We show the impacts and benefits of using formal verification in software development that must be compliant with the IEC 61508 standards, especially for SIL 3 and SIL 4 software development. We conclude by detailing specific formal verification techniques and tools available today for use in a state-of-the-art model-based development environment. We focus on the verification of safety requirements, involving control-logic aspects as well as data computation aspects of embedded software. We explain how to relate this model-checking activity with the objectives of the software life cycle process described in the IEC 61508 standards.Figures on the use of the SCADE product and its Design Verifier module on several realistic safety-related automotive applications illustrate the presentation.


    Zugriff

    Zugriff prüfen

    Verfügbarkeit in meiner Bibliothek prüfen

    Bestellung bei Subito €


    Exportieren, teilen und zitieren



    Titel :

    Formal Verification for Model-Based Development


    Weitere Titelangaben:

    Sae Technical Papers


    Beteiligte:
    Bouali, Amar (Autor:in) / Dion, Bernard (Autor:in)

    Kongress:

    SAE 2005 World Congress & Exhibition ; 2005



    Erscheinungsdatum :

    2005-04-11




    Medientyp :

    Aufsatz (Konferenz)


    Format :

    Print


    Sprache :

    Englisch




    Formal verification for model-based development

    Bouali,A. / Dion,B. / Esterel Technologies,FR | Kraftfahrwesen | 2005


    Formal Verification in Model Based Development

    Hocking, Ashlie B. / Knight, John C. / Aiello, M. Anthony et al. | SAE Technical Papers | 2015


    Formal verification in model based development

    Hocking,A.B. / Knight,J.C. / Aiello,M.A. et al. | Kraftfahrwesen | 2015


    2005-01-0781 Formal Verification for Model-Based Development

    Bouali, A. / Dion, B. / Society of Automotive Engineers | British Library Conference Proceedings | 2005


    SIMULATION-BASED AND FORMAL VERIFICATION OF DOMAIN-SPECIFIC LANGUAGE MODEL

    Chhaya, Bharvi N. / Jafer, Shafagh | TIBKAT | 2020