A Model Checking Approach for Multi-core Time Partitions Design

In many areas of safety-critical applications multiple applications must execute on a common machine without disturbing each other. Thus spatial and temporal isolation of each application must be guaranteed. In this paper we address the temporal isolation aspect which can be tackled using time partitioning. We propose a technique for automated design of multi-core time partitions based on characteristics of application workload. The work goes beyond recent work in the literature by effectively computing the parameters of multi-core time partitions, a task which is traditionally done manually by the system designer.