Combining test and proof in MBAT: An aerospace case study

In the aerospace industry, it has become possible to use formal analysis results as certification evidence thanks to the new version of the standard DO-178C and its formal methods supplement DO-333. Furthermore, formal proof has a high potential of cost reduction. On the other hand, it is not possible to replace testing completely by formal analysis, because the latter only considers more or less abstract models of the system under analysis, and can fail due to a too high complexity. But since certain verification tasks can be carried out by formal analysis with an advantage compared to testing, the question arises how both techniques, i.e. proof and test, can be combined in the best way. The European project MBAT gives answers to this question, and in this article we show how the combined approach has been applied to a relevant use case from Rockwell Collins.