Deployment and Scheduling Synthesis for Mixed-Critical Shared-Memory Applications

This paper presents an efficient approach for generating suitable system architectures for embedded systems efficiently. Thereby, we focus on a joint generation of schedules and deployment for mixed-criticality multicore architectures using shared memory. The presented approach computes task and message schedules that are optimized with respect to a global discrete time base. As part of the solution, our approach generates an optimized assignment of tasks to computation resources (cores) concerning local memory constraints of cores and criticality constraints of tasks.This approach is integrated into the Auto FOCUS3 tool-chain, using a formally defined model of computation with explicit data-flow and discrete-time semantics to develop multi-criticality embedded systems. Our approach relies on a symbolic encoding scheme, based on a system model that is derived from the system architecture. This paper provides a formalization describing the scheduling problem as a satisfiability problem using boolean formulas and linear arithmetic constraints. A state-of-the-art satisfiability modulo theory (SMT) solver is used to compute the joint schedule and deployment for such architectures. This paper demonstrates that state-of-the art satisfiability modulo theory solvers can be used to efficiently compute (safety-oriented) deployments including real-time task and communication schedules for mixed-criticality applications.