Integrating Formal Program Verication with Testing
Cyrille Comar, Johannes Kanig, Yannick Moy · 2012
Verication activities mandated for critical software are essential to achieve the required level of condence expected in life-critical or business-critical software. They are becoming increasingly costly as, over time, they require the development and maintenance of a large body of functional and robustness tests on larger and more complex applications. Formal program verication oers a way to reduce these costs while providing stronger guarantees than testing. Addressing verication activities with formal verication is supported by upcoming standards such as do-178c for software development in avionics. In the Hi-Lite project, we pursue the integration of formal verication with testing for projects developed in C or Ada. In this paper, we discuss the conditions under which this integration is at least as strong as testing alone. We describe associated costs and benets, using a simple banking database application as a case study.