Towards Scalable Verification of Commercial Avionics Software

We describe a model-based approach for the automated verification of avionics systems that has been applied in Honeywell for the certification of complex commercial avionics applications, such as flight controls and engine controls. The approach uses a symbolic analysis framework for MATLAB Simulink models, utilizing range arithmetic to represent both test cases and equivalence-class transformations within a model of behavioral requirements. Backwards search from a set of desired test-case values within the model is combined with forward-directed simulation to resolve constraints and compute values in the visited paths, leading to a set of model-level input/output values that produce the test cases. We also describe a common design flaw that was uncovered in an early design phase by utilizing this approach. We argue that finding such designs flaws is extremely difficult by alternative methods such as directed or random simulations and traditional model checkers. Utilizing our approach, Honeywell has achieved better than 20 speedup on average in certification costs compared to traditional analysis and testing methods, while maintaining scalability on complex real-life problems.