Integrating Formal Methods into Software Toolsets for Avionics Certification

Current practice in certification of avionics systems (e.g. DO-178B1) is centered on testing. The testing process has been prescribed to incorporate a semi-formal notion of completeness to demonstrate that the software correctly implements all its requirements, and nothing further. But in the last analysis, our confidence in modern avionics is based primarily on the successful completion of a test suite that, although extensive, is incomplete.