Towards Verifiability-Aware Variability Modeling using SysML v2 for Security- and Safety-Critical Avionics

The increasing need for configurable and reusable avionics system architectures introduces significant challenges in the systematic handling of variability across structure, behavior, and requirements. Current model-based systems engineering practices provide limited support for analyzing such variability in a consistent and verifiability-aware manner, particularly in early design phases. This paper presents a unified, SysML v2–based methodological framework for modeling, instantiating, and analyzing variability in avionics system architectures. The approach is evaluated using an avionics component case study featuring two alternative architectural design variants. A model-based trade-off analysis demonstrates that one variant enables automated verification, while the other alternative incurs significantly higher verification effort. The automatically verifiable architecture is selected based on objective, model-derived criteria. Formal verification evidence is provided to document the feasibility of the proposed solution.