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.


    Access

    Download


    Export, share and cite



    Title :

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


    Additional title:

    CEAS Aeronaut J


    Contributors:

    Published in:

    Publication date :

    2025-01-01




    Type of media :

    Article (Journal)


    Type of material :

    Electronic Resource


    Language :

    English





    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

    Free access

    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