Abstract Currently, the most widespread software quality assurance methods in the avionics domain are semi-automated reviews and testing. However, their effort grows disproportionately to the size of the system under development. Also, these methods cannot achieve exhaustive coverage due to the complexity of today’s avionics systems and their potentially infinite set of combinations of possible inputs and system states. Furthermore, the later software issues are detected in the development process, the more expensive it is to fix them. To overcome these issues, a model-driven verification approach for modeling and analyzing avionics systems in early phases of the development is presented. To this end, semantics is given to SysML v2 models by a mapping to a theorem prover encoding. The development of a dedicated SysML v2 profile supporting event-driven data flow specifications, the encoding of corresponding structures in the theorem prover Isabelle, and a generator creating theorems from SysML v2 models are presented. The approach is evaluated by formally proving a representative 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 demonstrates the added value for meeting typical safety requirements in the avionics domain. The results can be transferred from avionics to other domains, as well.


    Zugriff

    Download


    Exportieren, teilen und zitieren



    Titel :

    Model-driven development for functional correctness of avionics systems: a verification framework for SysML specifications


    Weitere Titelangaben:

    CEAS Aeronaut J


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

    Erschienen in:

    Erscheinungsdatum :

    01.01.2025




    Medientyp :

    Aufsatz (Zeitschrift)


    Format :

    Elektronische Ressource


    Sprache :

    Englisch





    Enhancing System Model Quality: Evaluation of the Systems Modeling Language (SysML)-Driven Approach in Avionics

    Kausch, Hendrik / Pfeiffer, Mathias / Raco, Deni et al. | AIAA | 2025

    Freier Zugriff

    Exploring SysML v2 for Model-Based Engineering of Safety-Critical Avionics Systems

    Ahlbrecht, Alexander / Lukic, Bojan / Zaeske, Wanja et al. | IEEE | 2024


    High-quality interface specifications with SysML modelling

    Lauscher, Thoma / Fischer, Christian / Hiebenthal, Thorsten | IuD Bahn | 2011