Verification activities mandated for critical software are essential to achieve the required level of confidence 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 verification offers a way to reduce these costs while providing stronger guarantees than testing. Addressing verification activities with formal verification is supported by recent standards such as DO-178C for software development in avionics.
In the Hi-Lite project, we pursue the integration of formal verification with testing for projects developed in C or Ada. We present an open source verification framework based on the GNAT compiler for Ada, which allows combining the results of testing and formal verification of Ada programs. We benefit from the recent update of the Ada language, which includes richer expressions and contracts on functions. We show that this combination of verification techniques can be as strong as testing alone, while allowing the user to choose the most cost-effective technique for every function.
