  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.
