For safety-critical real-time embedded systems, the worst-case execution time (WCET) analysis—
determining an upper bound on the possible execution times of a program—is an important part
of the
For safety-critical real-time embedded systems, the worst-case execution time (WCET) analysis—
determining an upper bound on the possible execution times of a program—is an important part
of the system verification. Multi-core processors share resources (e.g. buses and caches) between
multiple processor cores and, thus, complicate the WCET analysis as the execution times of a
program executed on one processor core significantly depend on the programs executed in parallel
on the concurrent cores. We refer to this phenomenon as shared-resource interference.
This thesis proposes a novel way of modeling shared-resource interference during WCET
analysis. It enables an efficient analysis—as it only considers one processor core at a time—and it
is sound for hardware platforms exhibiting timing anomalies. Moreover, this thesis demonstrates
how to realize a timing-compositional verification on top of the proposed modeling scheme. In
this way, this thesis closes the gap between modern hardware platforms, which exhibit timing
anomalies, and existing schedulability analyses, which rely on timing compositionality. In addition,
this thesis proposes a novel method for calculating an upper bound on the amount of interference
that a given processor core can generate in any time interval of at most a given length. Our
experiments demonstrate that the novel method is more precise than existing methods.
Michael Jacobs
Michael Jacobs is a programmer from Saarbrücken, Germany. From 2011 to 2017, he worked as a researcher at Saarland University. Since 2018, he has worked as a software engineer in the industry.
real-time worst-case execution time multi-core processors shared bus shared resources interference formal methods