Zur Seitenansicht


Replacing Conjectures by Positive Knowledge: Inferring Proven Precise Worst-Case Execution Time Bounds Using Symbolic Execution
Verfasser / Verfasserin Knoop, Jens In der Gemeinsamen Normdatei der DNB nachschlagen ; Kovács, Laura In der Gemeinsamen Normdatei der DNB nachschlagen ; Zwirchmayr, Jakob
Erschienen in
Journal of Symbolic Computation, 2017, Jg. 80, S. 101-124
ErschienenElsevier, 2017
Submitted version
DokumenttypAufsatz in einer Zeitschrift
Schlagwörter (EN)Worst-Case Execution Time (WCET) Analysis / Static Symbolic Execution / Symbolic Computation / Automated Reasoning
Projekt-/ReportnummerERC Starting Grant 2014 SYMCAR 639270
Projekt-/ReportnummerWallenberg Academy Fellowship 2014 - TheProSE
Projekt-/ReportnummerSwedish VR grant GenPro D0497701
Projekt-/ReportnummerAustrian Science Fund (FWF): RiSE S11409-N23
Projekt-/ReportnummerEU FP7 COST Action IC 1202 Timing Analysis on Code-Level (TACLe)
URNurn:nbn:at:at-ubtuw:3-3335 Persistent Identifier (URN)
 Das Werk ist frei verfügbar
Replacing Conjectures by Positive Knowledge: Inferring Proven Precise Worst-Case Execution Time Bounds Using Symbolic Execution [0.85 mb]
Zusammenfassung (Englisch)

Embedded real-time software systems (ESS) play an important role in almost every aspect of our daily lives. We do rely on them to be functionally correct and to adhere to timing-constraints ensuring that their computational results are always delivered in time. Violations of the timing-constraints of a safety-critical ESS, such as an airplane or a medical control device, can have disastrous economic and social consequences. Identifying and correcting such violations is therefore an important and challenging research topic. In this article we address this challenge and describe a rigorous approach for the timing analysis of programs and for proving its results precise.

In practice most important is the worst-case execution time (WCET) of an ESS, that is, the maximal running time of the system on a specified hardware. A WCET analysis needs to provide a formal guarantee that a system meets its timing-constraints even in the worst case. This requires to compute a safe and tight bound for the execution time of a program. Existing WCET tools, however, are usually not able to guarantee that there is a feasible system trace that takes indeed as long as stated by the computed execution time bound: often, due to the employed abstractions during static analysis a computed WCET bound overestimates the actual WCET bound, since loop bounds and other timing-relevant program properties their computation is based on are computed for spurious infeasible system traces that can be ruled out by a path-sensitive program abstraction and analyzing program resources.

In this article we present an approach for inferring and proving WCET bounds precise. This approach guarantees that the WCET bound is computed for a feasible system trace. This is achieved by combining WCET computation with path-wise symbolic execution in an abstraction refinement loop. This way, symbolic execution can be targeted and limited to relevant program parts thereby taming and avoiding the usually prohibitive computational costs of symbolic execution with a full path coverage. Moreover, our approach improves the quality of the underlying WCET analysis, since it automatically tightens the bound until it is proven precise, thereby improving the precision of the initially computed WCET bound.

Our overall approach is an anytime algorithm, i.e., it can be stopped at any time without violating the soundness of its results. If run until termination, the WCET bound is proven precise, by automatically inferring additional constraints from spurious traces and using these constraints in the abstraction refinement.

We implemented our approach in the r-TuBound WCET toolchain and tested it on challenging benchmarks from the WCET community. Our experimental results underline the advantage of using symbolic methods for proving WCET bounds precise, at a moderate cost.

Das PDF-Dokument wurde 19 mal heruntergeladen.