Deploying critical software with certification and frequent updates is a major challenge. Exhaustive testing of safety-critical systems is not possible due to the exponential growth of test cases; extensive but non-exhaustive testing is potentially unsafe; and while formal methods (FM) can provide full coverage, many FM tools have been found to be defective, producing the wrong output and leaving software practitioners understandably hesitant to trust FM tools.

The objective of this one-year project was to develop explanation methods (XM) as add-on tools to FM, producing explanations for why an FM tool deemed certain claims to be true. This will improve the use of formal methods and the adoption of FM tools to simultaneously achieve safety and reduce time to fielding. Certification is a very large part of the cost and schedule of many engineering projects, and it hampers our ability to develop new systems to respond to new threats. Explanations help ease the certification process because FM can reduce the need for extensive (costly and time consuming) testing and explanations can make it possible for software practitioners to trust FM tools.

As part of this project, we surveyed the state of the art on explainability to generate ideas, developed XM and an add-on tool for schedulability test where it outputs “no” or “yes,” and evaluated these solutions. We focused on software verification techniques and making them explainable; so rather than simply outputting a Boolean (safe/unsafe) based on input (a model), the tool included an explanation of how the output was produced based on this particular input.

Qualifying FM tools can be expensive. However, with XM techniques, FM tools can be used without tool qualification and still align to standards. In the future, these techniques can be used to increase the speed and reduce the cost of software development.