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
- Technischer Abschlussbericht
- Fallstudie Bahnübergang
- Fallstudie Blinkersteuerung
- RulesDSL Demo-Toolkit
- J. Peleska, W. Huang: “Exhaustive Model-Based Equivalence Class Testing”. Submitted to ICTSS 2013.
- J. Peleska. “Industrial-Strength Model-Based Testing – State of the Art and Current Challenges“. Proc. of MBT’13. Serie: EPTCS, Volume 111, S. 3-28 (2013). DOI:10.4204/EPTCS.111.1
- J. Brauer, J. Peleska and U. Schulze: “Efficient and trustworthy tool qualification for model-based testing tools”. Proc. of ICTSS’12, Springer. Serie: LNCS, Volume 7641, S. 8–23.
- M. Sulzmann, J. Nicklisch-Franken, A. Zechner: “Traceability and Evidence of Correctness of EDSL Abstractions“. Proc. of PEPM’13, ACM. S. 71-74.
- M. Sulzmann, A. Zechner: “Model Checking DSL-Generated C Source Code“. Proc. of SPIN’12, Springer. Serie: LNCS, Volume 7385, S. 241-247.
- H. Günther, S. Milius, O. Möller: “On the formal verification of systems of synchronous software components“. Proc. of SAFECOMP’12, Springer. Serie: LNCS, Volume 7612, S. 291-304. Extended version available here.
- M. Sulzmann, A. Zechner: “Constructive Finite Trace Analysis with Linear Temporal Logic“. Proc. of TAP’12, Springer. Serie: LNCS, Volume 7305, S. 132-148.
- O. Möller: “Benchmark Analysis of GTL-Backends using Client-Server Mutex“. Whitepaper, Februar 2012.
- H. Günther, R. Hedayati, H. Löding, S. Milius, O. Möller, J. Peleska, M. Sulzmann, A. Zechner: “A framework for formal verification of systems of synchronous components“. Vorgestellt auf dem MBEES 2012 Workshop.
- M. Sulzmann, A. Zechner, R. Hedayati: “Run-Time Testing with Sequence LTL“. Technischer Bericht, Dezember 2011.
- J. Peleska, A. Honisch, F. Lapschies, H. Löding, H. Schmid, P. Smuda, E. Vorobev, C. Zahlten: “A Real-World Benchmark Model for Testing Concurrent Real-Time Systems in the Automotive Domain“. Proc. of ICTSS 2011, Springer. Serie: LNCS, Volume 7019, S. 146-161.