
RÃ©sumÃ© :
In an embedded realtime system (ERTS), realtime tasks (software) are typically
executed on a multicore sharedmemory platform (hardware). The number of cores
is usually small, contrasted with a larger number of complex tasks that share
data to collaborate. Since most ERTSs are safetycritical, it is crucial to
rigorously verify their software against various realtime requirements under
the actual hardware constraints (concurrent access to data, number of cores).
Both the realtime systems and the formal methods communities provide elegant
techniques to realize such verification, which nevertheless face major
challenges. For instance, model checking (formal methods) suffers from the
statespace explosion problem, whereas schedulability analysis (realtime
systems) is pessimistic and restricted to simple task models and schedulability
properties. In this paper, we propose a scalable and generic approach to
formally verify ERTSs. The core contribution is enabling, through joining the
forces of both communities, compositional verification to tame the statespace
size. To that end, we formalize a realistic ERTS model where tasks are complex
with an arbitrary number of jobs and critical sections, then show that
compositional verification of such model is possible, using a hybrid approach
(from both communities), under the stateoftheart partitioned fixedpriority
(PFP) with limited preemption scheduling algorithm. The approach consists of
the following steps, given the above ERTS model and scheduling algorithm.
First, we compute finegrained data sharing bounds for each critical section
that reads or writes some data from the shared memory. Second, we generalize an
algorithm that, aware of the data sharing bounds, computes an affinity
(taskcore allocation) guaranteeing the schedulability of hardrealtime (HRT)
tasks. Third, we devise a timed automata (TA) model of the ERTS, that takes
into account the affinity, the data sharing bounds and the scheduling algorithm,
on which we demonstrate that various properties can be verified compositionally,
\ie on a subset of cores instead of the whole ERTS, therefore reducing the
statespace size. In particular, we enable the scalable computation of tight
worstcase response times (WCRTs) and other tight bounds separating events on
different cores, thus overcoming the pessimism of schedulability analysis
techniques. We fully automate our approach and show its benefits on three
realworld complex ERTSs, namely two autonomous robots and on an automotive case
study from an industrial challenge.
