Automated creation of safety in embedded software
This 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. The 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.
Even though our prototype implementation concentrates on source code verification tasks (as shown in a collaborative project with Airbus), the framework can be also used for other artefacts in the software development process including requirements and design.
Our continuous and evidential tool integration framework is inspired and closely related to SRI’s Evidential Tool Bus (ETB), which is a distributed workflow-based tool integration framework for constructing claims supported by evidence.
The expected benefits of using of our evidential and continuous tool integration framework include:
The main outcome of the project is a Java implementation of the ETB framework. In addition, the project also delivers a solving engine for distributed datalog programs with negation. Note that Datalog is used as a scripting language for writing verification workflows and running them on ETB.
Internal and through different projects (like AirbusFM in the past and now SPARTA)