Enabling in-field integration in critical embedded systems
In this thesis, I take up the idea of in-field integration for critical embedded systems that are subject to real-time, safety and security constraints. Component-based operating systems and service-oriented architectures already equip software systems with flexibility and adaptivity. However, in critical application domains, assurance must be provided for critical requirements, which complicates making changes after the initial deployment as these require re-verification. Automating a significant part of the integration process so that it can be moved into the system itself could enable self-controlled updates and adaptations. Yet, the current trend towards more dynamic high-performance embedded processing platforms further increases platform complexity. The growing complexity further challenges the integration and assurance process as well as the faithfulness of model-based methods used for formal verification. This thesis hosts several scientific contributions to these challenges:
It presents a model-based integration framework for component-based systems that automates composition and verification supported by a backtracking search for conflict resolution. Microkernel-oriented component-based operating systems provide strong spatial isolation which is required for security and safety as well as modularity. I further concentrate on the verification of latency requirements during an automated in-field integration. Since existing response-time analyses do not appropriately reflect the nature of explicit communication, its scheduling effects and shared services in component-based operating systems, I develop a novel task model and an accompanying formal response-time analysis. In order to close the model/implementation gap, I further present three runtime monitoring mechanisms: a novel lightweight budget-based scheduling technique to enforce model assumptions on execution times, an asynchronous supervision of budget curves to identify model deviations and trigger long-term adaptations and re-verification, and a latency monitoring scheme across multiple components that enables reactive countermeasures to immediately handle violations of critical latency requirements.
In dieser Arbeit widme ich mich der automatisierten Integration kritischer eingebetteter Systeme, die Echtzeitanfordernungen sowie Anforderungen zur Betriebs- und Datensicherheit unterworfen sind. Zwar statten komponentenbasierte Betriebssysteme und serviceorientierte Architekturen die Softwaresysteme bereits mit Flexibilität und Anpassungsfähigkeit aus, jedoch muss dabei die Einhaltung kritischer Anforderungen sichergestellt werden. Nachträgliche Änderungen erfordern deshalb eine erneute Verifizierung. Abhilfe kann hierbei die Automatisierung eines wesentlichen Teils des Integrations- und Absicherungsprozesses schaffen, sodass dieser in das System selbst verlagert werden kann. Eine besondere Herausforderung stellt dabei der aktuelle Trend zu dynamischeren und leistungsfähigeren eingebetteten Verarbeitungsplattformen dar, welcher die Plattformkomplexität erhöht. Diese Arbeit enthält mehrere wissenschaftliche Beiträge zu diesen Herausforderungen:
Sie stellt ein modellbasiertes Integrationsframework für komponentenbasierte Systeme vor, das die Komposition und Verifikation automatisiert und von einer Backtracking-Suche zur Konfliktlösung unterstützt wird. Mikrokernel-orientierte, komponentenbasierte Betriebssysteme bieten eine starke räumliche Isolation, die für Daten- und Betriebssicherheit sowie Modularität erforderlich ist. Des Weiteren konzentriere ich mich auf die Verifikation von Latenzanforderungen während einer automatisierten Integration. Da bestehende Antwortzeitanalysen die Natur der expliziten Kommunikation, deren Scheduling-Effekte und gemeinsam genutzte Dienste in komponentenbasierten Betriebssystemen nicht angemessen widerspiegeln, entwickle ich ein neuartiges Task-Modell und eine begleitende formale Antwortzeitanalyse. Um die Lücke zwischen Modell(-annahmen) und Implementierung zu schließen, stelle ich außerdem drei Laufzeitüberwachungsmechanismen vor: ein neuartiges, leichtgewichtiges, budgetbasiertes Scheduling-Verfahren zur Durchsetzung von Modellannahmen über Ausführungszeiten, eine asynchrone Überwachung von Budgetkurven, um Modellabweichungen zu identifizieren und langfristige Anpassungen bzw. eine erneute Verifizierung auszulösen, sowie ein Latenzüberwachungsschema über mehrere Komponenten, das reaktive Gegenmaßnahmen ermöglicht, um Verstöße gegen kritische Latenzanforderungen in Echtzeit zu behandeln.
Preview
Cite
Access Statistic

Rights
Use and reproduction:
All rights reserved