Our two-step code review process combines static analysis with other formal software analysis methods such as model checking, weakest precondition generation and testing. In the first step, the code review process applies a set of static analysis tools, each of which may be specialised in different aspects of the code, to generate an initial review report. Some tools may help identify coding defects such as resource leak, null pointer dereference, array out of bound, etc. Other tools may help to ensure certain coding standards, such as MISRA, are not violated. The process can also incorporate reviews from human code reviewers into the initial review report. In the second step, the code review process employs more powerful formal analysis methods in an efficient way by using insights from the initial review to generate a more refined review report.

The framework can be applied for automating the creation of safety (and possibly also security) cases for embedded software. As the framework is based on an evidential integration of formal analysis techniques, including static analysis, model checking, and test case generation as mandated for example by the DO-333 formal methods supplement of DO-178C, with more traditional techniques such as reviews. This tool integration framework is evidential as safety cases in Goal Structuring Notation(GSN) are automatically generated from pre- defined safety case patterns and by chaining generated evidences from the individual verification tools for particular safety claims. Our integration framework is continuous in that it is based on a continuous integration framework for Software development; in our prototype implementation we are using the widely used Jenkins continuous integration framework. In this way, (partial) safety cases are continuously updated, and consequently our framework directly supports the implementation of agile development processes for safety-critical Software, and the constructed safety case may actually drive further developments. Finally, even though our prototype implementation concentrates on software verification tasks, the basic framework can readily be used for other artefacts in the software development process in- cluding requirements and architectural design.