Real-time systems (RTSs) are at the heart of numerous safety-critical applications. An RTS typically consists of a set of real-time tasks (the software) that execute on a multicore shared-memory platform (the hardware) following a scheduling policy. In an RTS, computing inter-core bounds, i.e., bounds separating events produced by tasks on different cores, is crucial. While efficient techniques to over-approximate such bounds exist, little has been proposed to compute their exact values. Given an RTS with a set of cores C and a set of tasks T , under partitioned fixed- priority scheduling with limited preemption, a recent work by Foughali, Hladik and Zuepke (FHZ) models tasks with affinity c (i.e., allocated to core c in C) as a Uppaal timed automata (TA) network Nc. For each core c in C, Nc integrates blocking (due to data sharing) using tight analytical formulae. Through compositional model checking, FHZ achieved a substantial gain in scalability for bounds local to a core. However, computing inter-core bounds for some events of interest E, produced by a subset of tasks TE with different affinities CE, requires model checking the parallel composition of all TA networks Nc for each c in CE, which produces a large, often intractable, state space. In this paper, we present a new scalable approach based on exact abstractions to compute exact inter-core bounds in a schedulable RTS, under the assumption that tasks in TE have distinct affinities. We develop a novel algorithm, leveraging a new query that we implement in Uppaal, that computes for each TA network Nc in NE an abstraction A(Nc) preserving the exact intervals within which events occur on c, therefore drastically reducing the state space. The scalability of our approach is demonstrated on the WATERS 2017 industrial challenge, for which we efficiently compute various types of inter-core bounds where FHZ fails to scale.

翻译：实时系统（RTS）是众多安全关键应用的核心。典型的RTS由一组实时任务（软件）组成，这些任务在多核共享内存平台（硬件）上按照调度策略执行。在RTS中，计算跨核边界（即分离不同核心上任务所产生事件的边界）至关重要。尽管存在高效过近似此类边界的技术，但关于精确值计算的研究尚少。针对采用有限抢占式分区固定优先级调度的RTS，若给定核心集合C和任务集合T，Foughali、Hladik和Zuepke（FHZ）近期的工作将亲和性为c（即分配到核心c∈C）的任务建模为Uppaal时间自动机（TA）网络Nc。对于每个核心c∈C，Nc通过紧凑解析公式整合因数据共享导致的阻塞。通过组合模型检验，FHZ在核心局部边界的可扩展性方面取得了显著提升。然而，计算由具有不同亲和性CE的任务子集TE产生的某些关注事件E的跨核边界，需要对CE中每个c对应的所有TA网络Nc进行并行组合模型检验，这将产生庞大且通常难以处理的状态空间。本文提出一种基于精确抽象的可扩展新方法，在TE中任务具有不同亲和性的假设下，计算可调度RTS中的精确跨核边界。我们开发了一种新颖算法，利用在Uppaal中实现的新查询，为NE中的每个TA网络Nc计算抽象模型A(Nc)，该模型保留事件在核心c上发生的精确时间区间，从而大幅缩减状态空间。我们通过WATERS 2017工业挑战验证了方法的可扩展性，成功高效计算了FHZ无法扩展处理的多种类型跨核边界。