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.