Evidential Tool Bus

Evidential Tool Bus

A framework for continuous and accountable software certification

Evidential Tool Bus

The complexity of embedded software and increasing demands on safety has already outpaced the capabilities of current verification and certification methods. The framework of Evidential Tool Bus (ETB2) provides container-based services that automatically and continuously execute verification workflows in a decentralized manner to generate formal safety arguments supported by accountable evidence that corroborates safety of the software.

Project description

The project is aimed at devising techniques for establishing safety claims for a given software by means of decentralized arguments and supporting evidence. On one hand, the project develops formal and semi-formal languages for specifying safety argumentation patterns that can be found in certification standards and guidelines as well as good industrial practices. The languages should also be expressive enough to describe resulting safety claims and arguments.

On the other hand, the project develops algorithms for the decentralized execution of safety arguments where multiple entities will collaborate to establish a given claim. It is important to devise a secure way of exchanging claims and supporting evidence between interacting entities. Finally, the project gives special focus to emerging applications of AI by developing safety argumentation patterns and sufficient evidence artifacts for software with learning-enabled components.

Research contribution

ETB2 is built on the following three corner stones:

Formal Arguments: ETB2 formalizes the policies used in safety arguments as logical specifications in Cyberlogic, a first-order attestation logic for evidential transactions. These policies are programed in the form of distributed logic programs. These specifications combine logical inference with evidences generated by verification workflows. This means that safety arguments used in safety cases have precise semantics, thus enabling certification assessment to be carried out incrementally and continuously in an automated fashion.

Workflows as Services: Automated software verification workflows, specified in Cyberlogic, enable the automated generation of evidence by executing existing state-of-the-art software verification tools. Services are decentralized, container-based components that provide such verification workflows, thus supporting scalability in operational environments.


Internal and through different projects

Project duration


Dr. Tewodros Beyene

Your contact

Dr. Tewodros Beyene

+49 89 3603522 24

More information

Project partner


  • 2018 Evidential and Continuous Integration of Software Verification Tools Tewodros Beyene and Harald Rueß In Formal Methods, pages 679-685, Cham, Springer International Publishing. Details BIB