Currently, the most wide-spread quality assurance methods in industry are testing and manual reviews, but their costs grow disproportionately with the system size and they cannot achieve exhaustive coverage. To overcome these issues, a model-based verification approach for analyzing cyber-physical systems early in the development phase is presented. A semantics is given to SysML v2 models by a mapping into a (theorem prover encoding of a) data flow formalism. The creation of a SysML profile supporting event-driven and state-based specifications, the encoding of corresponding data flow structures in the theorem prover Isabelle, and a code generator from SysML to Isabelle is shown. The approach is evaluated by formally proving a selected liveness property of a hierarchical system model from the avionics domain. Since liveness properties can be negated only by infinite data sequences and thus cannot be covered exhaustively by testing, this case study suitably demonstrates the added value of our methodology. Finally, this MBSE framework for early design analysis can lead to an optimization of the architecture layout (i.e. reducing the number of required avionics components), which in turn can lead to the reduction of the avionics equipment weight, and thus of the energy consumption, producing less CO2 emissions.


    Zugriff

    Zugriff prüfen

    Verfügbarkeit in meiner Bibliothek prüfen

    Bestellung bei Subito €


    Exportieren, teilen und zitieren



    Titel :

    Correct and Sustainable Development Using Model-based Engineering and Formal Methods


    Beteiligte:
    Kausch, Hendrik (Autor:in) / Pfeiffer, Mathias (Autor:in) / Raco, Deni (Autor:in) / Rumpe, Bernhard (Autor:in) / Schweiger, Andreas (Autor:in)


    Erscheinungsdatum :

    2022-09-18


    Format / Umfang :

    1834461 byte





    Medientyp :

    Aufsatz (Konferenz)


    Format :

    Elektronische Ressource


    Sprache :

    Englisch