Allowing Flexibility in Critical Systems: The EPOC Framework

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.