Formal verification may play a central role in the development of safe controllers, such as those found in electric drives or (semi-)autonomous vehicles, whose complexity arises from the coexistence of mechanical and electrical subsystems with sophisticated electronic controllers that must implement high-level control policies according to different driving modes, while optimizing several objectives, such as safety first and foremost, efficiency, and performance among others. Model-driven development resorts to simulation to assess how well the various requirements and constraints are satisfied, but there is a growing awareness that more rigorous methods are needed to achieve the required levels of safety. This paper proposes a conceptual framework for the development of complex systems based on (i) higher-order logic specification, (ii) verification by theorem proving, and (iii) tight integration of verification with model-driven development and simulation. This framework addresses both digital and analog systems, as illustrated with some examples in different fields including implantable biomedical systems, autonomous vehicles, and electric valve actuation.


    Zugriff

    Download


    Exportieren, teilen und zitieren



    Titel :

    Formal verification in the loop to enhance verification of safety-critical cyber-physical systems



    Erscheinungsdatum :

    2019-01-01



    Medientyp :

    Aufsatz (Zeitschrift)


    Format :

    Elektronische Ressource


    Sprache :

    Englisch



    Klassifikation :

    DDC:    629



    Formal Verification of Safety-Critical Aerospace Systems

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


    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 requirements on complex systems

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


    Formal Verification Method for Safety Diagnosis Software

    Narisawa, Fumio / Matsubara, Masahiro / Nishi, Masataka et al. | SAE Technical Papers | 2015