Konstruktion und Verifikation eingebetteter echtzeitfähiger Steuerungssoftware und ihrer Transformation in ausführbaren Code unter besonderer Berücksichtigung von Multicore und Adaptivität
Final Report Abstract
Die Entwicklung eingebetteter Echtzeitsysteme, wie z.B. Flugzeuge, Autos, etc., wird zunehmend modellbasiert durchgeführt. Modelle höherer Abstraktionsebenen werden dabei schrittweise zu niedrigeren Modellebenen bis hin zum ausführbaren Code transformiert. In bisherigen Ansätzen wird die Korrektheit dieser Transformationsschritte bezüglich Sicherheits-, Lebendigkeits- und Echtzeiteigenschaften nicht garantiert. Um dieses Problem zu lösen, haben wir im Rahmen des VATES-Projekts eine Methodik zur durchgehenden computergestützten Verifikation von eingebetteten Echtzeitsystemen über alle Abstraktionsebenen hinweg entwickelt. Korrektheitsbeweise führen wir dabei sowohl in Theorembeweisern als auch in Model Checkern durch. Als Fallstudie verwenden wir das Echtzeitbetriebssystem BOSS und verschiedene selbst-adaptive Systeme, die wir in der zweiten Phase des Projekts adressieren. Auf der Modellebene betrachten wir exemplarisch den Prozesskalkül Timed CSP, der dazu geeignet ist, nebenläufige Echtzeitsysteme zu beschreiben. Um Beweise in diesem Kalkül computergestuützt, d.h. garantiert korrekt, durchführen zu können, haben wir dessen Syntax und Semantik im Theorembeweiser Isabelle/HOL formalisiert. Zur Beschreibung von Eigenschaften von Timed CSP Modellen haben wir eine zeitbehaftete Logik entwickelt. Weiterhin haben wir Bisimulationsrelationen formalisiert, mit denen Timed CSP Modelle unterschiedlicher Abstraktionsebenen formal in Beziehung gesetzt werden können. Die Verifikation mit Theorembeweisern ist üblicherweise sehr aufwändig, da Beweisschritte interaktiv vorgegeben werden müssen und nur zum Teil automatisiert werden können. Um ein Timed CSP System vor der aufwändigen, dafür aber korrekten, Verifikation im Theorembeweiser automatisiert analysieren zu können, haben wir Transformationen von Timed CSP nach Tock CSP und Timed Automata entwickelt, für die automatische Model Checker existieren. In der zweiten Projektphase haben wir selbst-adaptive Systeme betrachtet. Diese passen sich dynamisch an geänderte Umgebungen an, um ihre Systemziele bestmöglich zu erfüllen. Für deren skalierbare Verifikation haben wir einen Ansatz zur systematischen Beschreibung verteilter, selbst-adaptiver Echtzeitsysteme mit Timed CSP entwickelt. Durch unsere strikte Trennung von Adaptionsschicht und Systemschicht ermöglichen wir eine kompositionale Verifikation. Weiterhin haben wir gängige Design Patterns für die modellgetriebene Entwicklung von selbst-adaptiven Systemen in CSP formalisiert, womit die Analyse der Gemeinsamkeiten unterschiedlicher Design Patterns ermöglicht und deren Interoperabilität vereinfacht wird. Neben diesen formal rigorosen Ansätzen haben wir zusätzlich auch einen Entwicklungsansatz für selbst-lernende selbst-adaptive Systeme erarbeitet. Wir setzen dabei SystemC zur Systembeschreibung ein und integrieren Methoden des maschinellen Lernens, um die Adaptionslogik selbst dynamisch anzupassen. Die möglichen Auswirkungen dieser Anpassungen auf das System analysieren wir automatisiert mit Model Checkern für zeitbehaftete Automaten. Um (Timed CSP) Modelle höherer Abstraktionsebenen mit ausführbaren Code mechanisiert in Beziehung setzen zu können, haben wir eine generische Low-Level Sprache entwickelt und im Theorembeweiser Isabelle/HOL formalisiert. Dabei haben wir insbesondere operationale und denotationelle CSP-ähnliche Semantiken erarbeitet. Somit können formale Bezüge zwischen Modellebene und Code-Ebene über Bisimulationen und Verfeinerungsbegriffe hergestellt werden. Die wesentliche Herausforderung bei der Erstellung der Semantiken für unstrukturierte Low-Level Sprachen war dabei, diese kompositional zu entwerfen, d.h. dass einzelne Programmteile des Low-Level Programms in Isolation betrachtet werden können und Beweise über das Gesamtsystem davon abgeleitet werden können. Eine weitere Herausforderung bei dem Entwurf von Low-Level Sprachen war die Berücksichtigung der Verteilung von und der Kommunikation zwischen einzelnen Low-Level Programmen, wie es beispielsweise für Multi-Core-Systeme benötigt wird. Die Semantiken unserer Low-Level Sprache ermöglichen es uns, Code- und Modell-Ebene über Bisimulationen und formale Verfeinerungen in Beziehung zu setzen. Da sowohl Bisimulationen als auch formale Verfeinerungen Sicherheits-, Lebendigkeits-, und Echtzeiteigenschaften bewahren, können wir damit die Korrektheit zwischen Spezifikationsmodellen und implementiertem Code nachweisen. Um eine optimierte Implementierung von einem abstrakten Modell (manuell) zu erhalten, nutzen wir einen Prototyping-Ansatz, bei dem Events in CSP Prozessen an ausführbaren Code gebunden werden. Um den manuell erzeugten Low-Level Code schließlich mit Spezifikationsmodellen in (Timed) CSP in Beziehung zu setzen, haben wir zwei Ansätze entwickelt. Mit llvm2csp bieten wir die Möglichkeit, CSP Modelle aus Programmcode zu extrahieren. Diese Modelle können dann mittels der Standard-Verfeinerungsbegriffe von CSP mit den Spezifikationsmodellen in Beziehung gesetzt werden. Da die extrahierten CSP Modelle im allgemeinen sehr groß werden können, haben wir daneben einen Ansatz im Theorembeweiser entwickelt, um die Semantik des Spezifikationsmodells direkt mit dem Low-Level Code in Beziehung zu setzen. Um dies zu vereinfachen, stellen wir Hoare-Kalküle für unsere Low-Level Sprache zur Verfügung, um einzelne Beweisverpflichtungen effizienter durchführen zu können.
Publications
- Low level code verification based on CSP models. In M. Oliveira and J. Woodcock, editors, Brazilian Symposium on Formal Methods (SBMF 2009), pages 266–281. Springer, August 2009
M. Kleine and S. Helke
(See online at https://doi.org/10.1007/978-3-642-10452-7_18) - An Approach for Machine-Assisted Verification of Timed CSP Specifications. Innovations in Systems and Software Engineering - A NASA Journal, 2010
T. Göthel and S. Glesner
(See online at https://doi.org/10.1007/s11334-010-0126-z) - Formal modeling and verification of low-level software programs. In 10th International Conference on Qualtiy Software (QSIC 2010), pages 200–207. IEEE Computer Society, July 2010
B. Bartels and S. Glesner
(See online at https://doi.org/10.1109/QSIC.2010.67) - Simulating truly concurrent CSP. In Brazilian Symposium on Formal Methods (SBMF 2010). Springer, 2010
M. Kleine and J. W. Sanders
(See online at https://doi.org/10.1007/978-3-642-19829-8_9) - Specification, Verification and Implementation of Business Processes using CSP. In 4th IEEE International Symposium on Theoretical Aspects of Software Engineering, pages 145–154. IEEE Computer Society, 2010
M. Kleine and T. Göthel
(See online at https://doi.org/10.1109/TASE.2010.26) - The VATES-Diamond as a Verifier’s Best Friend. In Simon Siegler and Nathan Wasser, editors, Verification, Induction, Termination Analysis, volume 6463 of Lecture Notes in Computer Science, pages 81–101. Springer, 2010
S. Glesner, B. Bartels, T. Göthel, and M. Kleine
(See online at https://doi.org/10.1007/978-3-642-17172-7_5) - Towards the Semi-Automatic Verification of Parameterized Real-Time Systems using Network Invariants. In Proceedings of the 8th IEEE International Conference on Software Engineering and Formal Methods, 2010
T. Göthel and S. Glesner
(See online at https://doi.org/10.1109/SEFM.2010.38) - LLVM2CSP: Extracting CSP models from concurrent programs. In Third NASA Formal Methods Symposium, pages 500–505, 2011
M. Kleine, B. Bartels, T. Göthel, S. Helke, and D. Prenzel
(See online at https://doi.org/10.1007/978-3-642-20398-5_39) - The observer pattern applied to actor systems: A tla/tlc-based implementation analysis. In Sixth International Symposium on Theoretical Aspects of Software Engineering (TASE), pages 193–200, 2012
Rodger Burmeister and Steffen Helke
(See online at https://doi.org/10.1109/TASE.2012.15) - Mechanized, compositional verification of low-level code. In JuliaM. Badger and KristinYvonne Rozier, editors, NASA Formal Methods, volume 8430 of Lecture Notes in Computer Science, pages 98–112. Springer, 2014
Björn Bartels and Nils Jähnig
(See online at https://doi.org/10.1007/978-3-319-06200-6_8) - Modular design and verification of distributed adaptive real-time systems based on refinements and abstractions. EAI Endorsed Transactions on Self-Adaptive Systems, 15(1):5:1–5:12, 2015
Thomas Göthel, Verena Klös, and Björn Bartels
(See online at https://doi.org/10.4108/sas.1.1.e5) - Formal models for analysing dynamic adaptation behaviour in real-time systems. In 3rd Workshop on Quality Assurance for Selfadaptive, Self-organising Systems (QA4SASO), pages 106–111. IEEE, 2016
Verena Klös, Thomas Göthel, and Sabine Glesner
(See online at https://doi.org/10.1109/FAS-W.2016.34) - Refinement-based verification of communicating unstructured code. In Software Engineering and Formal Methods - 14th International Conference, SEFM 2016, Held as Part of STAF 2016, Vienna, Austria, July 4-8, 2016, Proceedings, pages 61–75, 2016
Nils Jähnig, Thomas Göthel, and Sabine Glesner
(See online at https://doi.org/10.1007/978-3-319-41591-8_5) - Refinement-based modelling and verification of design patterns for self-adaptive systems. In 19th International Conference on Formal Engineering Methods (ICFEM), pages 157–173. Springer, 2017
Thomas Göthel, Nils Jähnig, and Simon Seif
(See online at https://doi.org/10.1007/978-3-319-68690-5_10) - Be prepared: Learning environment profiles for proactive rule-based production planning. In 44th Euromicro Conference on Software Engineering and Advanced Applications (SEAA), pages 89–96. IEEE, 2018
Verena Klös, Thomas Göthel, and Sabine Glesner
(See online at https://doi.org/10.1109/SEAA.2018.00024) - Comprehensible and dependable selflearning self-adaptive systems. Journal of Systems Architecture, 85-86:28–42, 2018
Verena Klös, Thomas Göthel, and Sabine Glesner
(See online at https://doi.org/10.1016/j.sysarc.2018.03.004) - Preserving liveness guarantees from synchronous communication to asynchronous unstructured low-level languages. In Jing Sun and Meng Sun, editors, Formal Methods and Software Engineering - 20th International Conference on Formal Engineering Methods (ICFEM), volume 11232 of Lecture Notes in Computer Science, pages 303–319. Springer, 2018
Nils Berg, Thomas Göthel, Armin Danziger, and Sabine Glesner
(See online at https://doi.org/10.1007/978-3-030-02450-5_18) - Runtime management and quantitative evaluation of changing system goals in complex autonomous systems. Journal of Systems and Software, 144:314–327, 2018
Verena Klös, Thomas Göthel, and Sabine Glesner
(See online at https://doi.org/10.1016/j.jss.2018.06.076)
