DOL-BIP-Critical: a tool chain for rigorous design and implementation of mixed-criticality multi-core systems

• Published in: Design automation for embedded systems 2018-06, Vol.22 (1-2), p.141-181
• Main Authors: Giannopoulou, Georgia, Poplavko, Peter, Socci, Dario, Huang, Pengcheng, Stoimenov, Nikolay, Bourgos, Paraskevas, Thiele, Lothar, Bozga, Marius, Bensalem, Saddek, Girbal, Sylvain, Faugere, Madeleine, Soulat, Romain, de Dinechin, Benoît Dupont
• Format: Article
• Language: English
• Subjects: Avionics; CAE) and Design; Certification; Circuits and Systems; Computation; Computer Science; Computer-Aided Engineering (CAD; Embedded Systems; Engineering; Mathematical models; Special Purpose and Application-Based Systems; Weight reduction
• ISSN: 0929-5585; 1572-8080
• DOI: 10.1007/s10617-018-9206-3

Mixed-criticality systems are promoted in industry due to their potential to reduce size, weight, power, and cost. Nonetheless, deploying mixed-criticality 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 specification, using a novel mixed-criticality aware model of computation (DOL-Critical), to correct-by-construction implementation, using the principle ‘what you verify is what you generate’ which is based on a novel variant of task automata. We demonstrate the applicability of our design flow with an industrial avionic test case on the state-of-the-art Kalray MPPA ® -256.