Scalable Computation of Inter-Core Bounds Through Exact Abstractions

A real-time systems (RTS) typically consists of a set of real-time tasks that execute on a multicore platform following a scheduling policy. In an RTS, computing inter-core bounds, i.e., bounds separating events occurring 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? C) as a Uppaaltimed automata (TA) network N_C. 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 T_E? T with different affinities C_E? C, requires model checking N_E=||_c? C_EN_c, i.e., the parallel composition of all TA networks N_c for each c? C_E, which often produces an 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 T_E have distinct affinities. We develop a new Uppaalquery, and a novel algorithm that computes, for each TA network N_c in N_1i, an abstraction A(N_c) preserving the exact intervals within which events occur on c. Then, we model check A(N_E)=||_c ? C_EA(N_c) (instead of N_E), therefore drastically reducing the state space. We demonstrate the scalability of our approach as we efficiently compute inter-core bounds for the WATERS 2017 industrial challenge, where FHZ fails to scale.