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

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.