Evidential Tool Bus

Evidential Tool Bus

Automatisierte Erstellung von Sicherheit in eingebetteter Software

Evidential Tool Bus

Gegenstand des Projekts Evidential Tool Bus (ETB) ist ein System zur automatischen Erstellung von Safety und eventuell auch Security Cases in Embedded Software.

Projektbeschreibung

Der hierbei verfolgte Ansatz ist die beweisgestützte Integration formaler Analysetechniken (z.B. statische Analyse, Model Checking und Testfallgenerierung, wie z.B. gefordert von DO-333, dem Begleitdokument zu formalen Methoden von DO-178C) mit traditionelleren Techniken wie Reviews. Das vorgestellte System zur Integration von Tools ist beweisgestützt, da es die automatische Generierung von in Goal Structuring Notation (GSN) dargestellten Safety Cases ermöglicht, und zwar ausgehend von vordefinierten Safety-Case-Mustern und durch die Verknüpfung von Beweisen der einzelnen Verifizierungstools zu spezifischen Sicherheitsaussagen. Es handelt sich hier um ein kontinuierliches Integrationssystem, da es auf einem kontinuierlichen Integrationssystem für Softwareentwicklung aufsetzt. Wir nutzen nämlich für unsere Prototyp-Implementierung das weit verbreitete kontinuierliche Jenkins-Integrationssystem. Dies ermöglicht eine kontinuierliche Aktualisierung von (partiellen) Safety Cases, sodass unser System die Implementierung agiler Entwicklungsprozesse für sicherheitskritische Software direkt unterstützt und der entwickelte Safety Case sogar Ausgangspunkt für Weiterentwicklungen sein kann.

Unsere Prototyp-Implementierung setzt zwar den Schwerpunkt auf die Verifizierung des Quellcodes – wie gezeigt in einem kollaborativen Projekt mit Airbus –, das System kann jedoch auch für andere Artefakte im Softwareentwicklungsprozess, u.a. Anforderungen und Design, verwendet werden.

Unser kontinuierliches und beweisgestütztes Tool-Integrationssystem ist in enger Anlehnung an den Evidential Tool Bus (ETB) von SRI entstanden, das ein verteiltes, Workflow-basiertes Tool-Integrationsystem zur beweisgestützten Erstellung von Aussagen ist.

Die Vorteile unseres beweisgestützten und kontinuierlichen Tool-Integrationssystems sind:

  1. eine Verringerung des Zertifizierungsaufwands durch automatische Generierung von Safety Cases,
  2. eine Verringerung der Zertifizierungsdauer durch die ständige Verfügbarkeit von Safety Cases bei jeder Iteration des agilen Entwicklungsprozesses,
  3. eine Erhöhung der Zuverlässigkeit des Sicherheitsarguments durch die Kombination sich ergänzender formaler Analysemethoden mit traditionellen Review-Methoden,
  4. eine sicherheitsgetriebene Softwareentwicklung durch frühzeitig mögliche Sicherheitsargumentation,
  5. die Verfügbarkeit integrierter, formaler und informeller Analysemethoden für das weite Feld der agilen Softwareentwicklung

Forschungsbeitrag

Das Hauptergebnis des Projekts ist eine Java-Implementierung des ETB-Systems. Zudem umfasst das Projekt eine Solving Engine für verteilte Datalogprogramme mit Negation. Datalog wird als Skriptsprache zur Erstellung von Verifizierungsworkflows und ihrer Abarbeitung in ETB verwendet.

Förderung

Intern und über verschiedene Projekte (u.a. AirbusFM in der Vergangenheit und nun SPARTA)

Projektdauer

Fortlaufend

Dr. Tewodros Beyene

Ihr Ansprechpartner

Dr. Tewodros Beyene

+49 89 3603522 24
beyene@fortiss.org

Projektpartner

SRI International