The Ektokernel Approach: A Composition Paradigm for Building Evolvable Safety-critical Systems from Unsafe Components

Abstract:

The goal of this project is to develop a tool-chain for composition of safety-critical cyber-physical systems from a small code base of verified components and a large code base of unverified commercial off-the- shelf components. Unlike tool-chains that aim to deliver end-to-end verified component code, starting from formal languages, specifications, or models, an explicit goal of this project is to accommodate large amounts of legacy code that is typically too complex to verify. Hence, rather than verifying an entire project code-base (or generating it from a formal model), the project develops safety solutions that allow for the majority of code to remain unverified. There are two fundamental ideas involved. The first lies in architectural advances that allow safety and timing properties of an entire system to be verified despite the presence of unverified components. The second presents a diagnostic subsystem that identifies and resolves causes of performance problems when they arise due to unverified code. Together, these ideas lead to guaranteed safety, predictable timing, and optimized performance in a system with a large percentage of unverified code.