Towards Scalable Verification of Commercial Avionics Software
Devesh Bhatt, Gabor Madl, David B. Oglesby, Kirk Schloegel · AIAA Infotech@Aerospace 2010 · 2010
We describe a model-based approach for the automated verification of avionics systems that has been applied in Honeywell for the certification of complex 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 test cases and equivalence-class transformations within a model diagram. Backwards search from a set of desired test-case values within the diagram is combined with forward-directed simulations from the inputs to resolve constraints and select values in the visited paths, leading to a set of diagram input/output values that produce the test case. Utilizing this approach, Honeywell has achieved 20 − 50× reduction in certification costs compared to traditional analysis and testing methods, while maintaining scalability on complex real-life problems. As an example of the efficiency of this verification method, we describe a common design flaw that was uncovered in the early design phases of avionics software. We argue that finding such designs flaws is extremely hard by alternative methods such as directed or random simulations and traditional model checkers. I.