DOL-BIP-Critical: A Tool Chain for Rigorous Design and Implementation of Mixed-Criticality Multi-Core Systems

Abstract

Mixed-criticality systems are promoted in industry due to their potential to reduce size, weight, power, and cost. Nonetheless, deploying mixedcriticality applications on commercial multi-core platforms remains a highly challenging problem. To name a few reasons: (i) Industrial mixed-criticality applications are usually complex reactive applications, which cannot be specified by traditional, e.g., dataflow-based, models of computation. Appropriate mixed-criticality models of computation built upon Vestal’s assumptions are missing; (ii) Scheduling such applications on multicores with shared resources, such as memory buses, requires that any timing interference among applications of different criticality is bounded in order to guarantee - the necessary for certification - temporal isolation and to enable incremental design; (iii) The implementation of isolation-preserving mixed-criticality schedulers is itself subject to certification. Hence, it needs to be not only efficient, but also provably correct. This paper proposes, for the first time, a complete design flow covering all aspects from the high-level specification of mixedcriticality applications and target architectures, to methods for scheduling and mapping optimization that ensure temporal isolation, to functional validation of the design based on formal methods, and finally to the correctby-construction code generation for the target platform. We demonstrate the applicability of our design flow with an industrial avionic test case on the state-of-the-art Kalray MPPA R -256.