Evidential Tool Bus

Evidential Tool Bus

Automated creation of safety in embedded software

Evidential Tool Bus

The project Evidential Tool Bus (ETB) proposes a framework for automating the creation of safety (and possibly also security) cases for embedded software.

Project description

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:

  1. reduced certification effort by automated generation of safety cases.
  2. reduced certification time by making safety-cases readily available during each iteration of the agile development process.
  3. increased confidence in the safety argument by combining complementing formal analysis methods with traditional review methods.
  4. safety-driven software development by enabling early safety-argumentation.
  5. integrated formal (and informal) analysis methods available for the masses of agile software development.

Project contribution

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.

Funding

Internal and through different projects (like AirbusFM in the past and now SPARTA)

Project duration

On going

Dr. Tewodros Beyene

Your contact

Dr. Tewodros Beyene

+49 89 3603522 24
beyene@fortiss.org

Project partner

SRI International