Allowing Flexibility in Critical Systems: The EPOC Framework

Die Software Konfiguration von sicherheitskritischen Systemen wie z.B. Automobilen wird heutzutage nur selten im Feld verändert. Dieses Vorgehen steht im starken Gegensatz zu anderen, nicht-kritischen Systemen. Hier ist es üblich auch beim Kunden noch Veränderungen an der Software durch Updates vorzunehmen. Beispiele sind Desktop Betriebssysteme, aber auch eingebettete Software von z.B. Routern oder Spielekonsolen. Einer der Faktoren, die eine entsprechende Flexibilität bei sicherheitskritischen Systemen erschwert, ist die nötige Zertifizierung des Updates. Der damit verbundene Aufwand führt dazu, dass nur zwingend notwendige Updates (z.B. um Fehler in vorhandener Software zu beheben) im Feld durchgeführt werden. Diese Dissertation präsentiert einen Ansatz, der eine größere Software-Flexibilität in sicherheitskritischen Systemen ermöglichen kann. Der Ansatz umfasst eine Software Architektur-Vorlage für eine Laufzeitumgebung, die ein komplexes Zugangskontrollverfahren lose mit einer schlanken Laufzeitumgebung verknüpft. Das Zugangskontrollverfahren sowie die Konfiguration der Laufzeitumgebung basieren auf sogenannten Kontrakten zwischen Applikationen und der Laufzeitumgebung. Diese Kontrakte spezifizieren relevante Eigenschaften der Applikationen sowie Randbedingungen, die nicht verletzt werden dürfen. Wenn die implementierte Zugangskontrolle zuverlässig genug ist um manuelle Re-Zertifizierung zu ersetzen, kann ein solcher Ansatz Software Flexibilität in sicherheitskritischen Systemen ermöglichen. Der Hauptbeitrag dieser Dissertation betrifft das Zugangskontrollverfahren. Hier wurde ein existierender Analyseansatz (Performanzanalyse), der zurzeit als Teil des Verifikationsprozesses im Automobilbereich eingesetzt wird, angepasst, so dass er verteilt in einem eingebetteten System ausgeführt werden kann. Eine Formalisierung des Problems in dieser Dissertation erlaubt eine Diskussion über Existenz und Qualität von Analyseergebnissen. Darüber hinaus kann mit Hilfe des Formalismus nachgewiesen werden, dass der vorgeschlagene verteilte Algorithmus korrekt ist. Als zweiten Aspekt befasst sich diese Arbeit mit der Laufzeit des vorgeschlagenen Algorithmus. Hier wird gezeigt, dass die Analyse in allen relevanten Fällen nach einer endlichen Anzahl von Schritten eine Lösung liefert. Eine empirische Studie der Laufzeit der einzelnen Schritte des Algorithmus rundet diese Diskussion ab. Als letzten Aspekt wird in dieser Arbeit eine Implementierung der präsentierten Algorithmen beschrieben. Die Diskussion zeigt, dass durch die lose Kopplung der Zugangskontrolle und der Laufzeitumgebung die Letztere nur geringfügig komplexer als zurzeit üblich wird. Currently, software-intensive safety-critical systems assume mostly static software configurations. This is in contrast to other, non-critical software intensive systems such as smart phones or gaming consoles, where software updates are common practice. One of the factors prohibiting flexibility in critical systems are existing certification processes. The effort necessary to re-certify the product after an update in many cases prohibits wide-spread in-field deployment of software, where it is not absolutely necessary (e.g. to fix bugs). This thesis presents an approach allowing flexibility in safety-critical systems. It presents a generic architecture template for a runtime environment, which loosely couples a potentially complex admission control scheme with a lean execution environment for operation. The admission control scheme as well as the configuration of the execution environment are based on contracts between the runtime environment and applications running on the system. In cases where the admission control scheme is sufficiently powerful to replace manual verification, such an approach could enable flexibility also in critical systems. The main contribution of this thesis concerns one modeling scheme that could back such an admission control scheme. This thesis focuses on system timing as one aspect of safety-critical systems. Here, an existing formal analysis method (Compositional Performance Analysis) is transformed into a distributed algorithm, which could back an admission control scheme in the proposed architecture. In order to prove the transformation tractable, a novel formalization of the existing modeling and analysis scheme is presented, which enables reasoning about quality and existence of solutions as well as applicable algorithms. As a second aspect, this thesis discusses under which circumstances the proposed algorithm yields results in bounded time and proposes a method to compute such a bound beforehand. This is mandatory, if such an admission control scheme is to be employed at runtime in a timing-critical system. This discussion encompasses a novel empirical evaluation of existing bounded-time schedulability analysis algorithms, which are an integral part of system analysis. For completeness, this thesis also addresses design aspects of the execution environment developed in the course of the associated research. The discussion shows that it is possible to add a sufficient amount of flexibility to an existing micro kernel to allow for in-field software updates without adding a tremendous amount of overhead. For the implementation, in many cases existing approaches from different domains where adapted. The novel aspect is tight integration of application contracts with the configuration of the micro-kernel allowing for self-configuration of applicable services. The overall discussion shows that complex admission control as well as software flexibility in critical systems is tractable in general. The implementation gives insight into the associated cost in terms of memory and computational overhead.