Navigation

VerSyKo

Verifikation von Systemen synchroner Software-Komponenten

Projektkoordinator: Dr. Stefan Milius @TU Braunschweig

Zeitraum: 1.1.2011 – 31.12.2012

Kooperationspartner

Verified Systems International GmbH
Informatik Consulting Systems AG

Förderung

Bundesministerium für Bildung und Forschung (BMBF)

Zusammenfassung

Das Ziel des Projekts ist die Entwicklung und Erprobung eines durchgängigen und für die Industriepraxis innovativen Ansatzes zur Modellierung und Verifikation der Software verteilter, sicherheitskritischer, eingebetteter Systeme. Im Zentrum des Vorhabens steht die modellbasierte Entwicklung und Prüfung asynchron kommunizierender verteilter Steuerungssysteme, die aus lokal synchron operierenden Komponenten aufgebaut sind. Im Projekt soll die „methodische Lücke“ zwischen synchronen Komponenten und asynchronem Gesamtsystem durch den Einsatz Domänen-spezifischer Formalismen geschlossen werden.

Im ersten Schritt wird eine geeignete domänenspezifische Modellierungssprache für GALS-Systeme aus SCADE-Komponenten und für Zusicherungen der Komponenten (Kontrakte) erstellt. Danach werden Modellprüfungsverfahren angewandt um globale Sicherheitseigenschaften zu verifizieren. Weitere Arbeitsschritte betreffen eine Testmethodik und Zuverlässigkeitsbetrachtungen des integrierten HW/SW-Systems durch stochastische Modellprüfung. Eine gründliche Evaluation der entwickelten Methoden und die Entwicklung von Best Practices anhand zweier realistischer industrieller Anwendungsfallstudien runden das Projekt ab.

Die TU Braunschweig koordiniert das Projekt und arbeitet bei der Erstellung der domänen-spezifischen Modellierungssprache, der Formalismen zur Kontraktspezifikation und der Entwicklung von Modellprüfungsverfahren mit.

Beteiligte Mitarbeiter @TU Braunschweig

Dr. Stefan Milius
Henning Günther

Veröffentlichungen