Combining Test and Proof in MBAT - An Aerospace Case Study

Michael Dierkes

2014

Abstract

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.

Paper Citation

in Harvard Style

Dierkes M. (2014). Combining Test and Proof in MBAT - An Aerospace Case Study . In Proceedings of the 2nd International Conference on Model-Driven Engineering and Software Development - Volume 1: MBAT, (MODELSWARD 2014) ISBN 978-989-758-007-9, pages 636-644. DOI: 10.5220/0004874906360644

in Bibtex Style

@conference{mbat14,
author={Michael Dierkes},
title={Combining Test and Proof in MBAT - An Aerospace Case Study},
booktitle={Proceedings of the 2nd International Conference on Model-Driven Engineering and Software Development - Volume 1: MBAT, (MODELSWARD 2014)},
year={2014},
pages={636-644},
publisher={SciTePress},
organization={INSTICC},
doi={10.5220/0004874906360644},
isbn={978-989-758-007-9},
}

in EndNote Style

TY - CONF
JO - Proceedings of the 2nd International Conference on Model-Driven Engineering and Software Development - Volume 1: MBAT, (MODELSWARD 2014)
TI - Combining Test and Proof in MBAT - An Aerospace Case Study
SN - 978-989-758-007-9
AU - Dierkes M.
PY - 2014
SP - 636
EP - 644
DO - 10.5220/0004874906360644