| 1. |
- Biere, Armin, et al.
(författare)
-
SmacC: A Retargetable Symbolic Execution Engine
- 2013
-
Ingår i: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - Cham : Springer International Publishing. - 1611-3349 .- 0302-9743. - 9783319024431 ; LNCS 8172, s. 482-486
-
Konferensbidrag (refereegranskat)abstract
- SmacC is a symbolic execution engine for C programs. It can be used for program verification, bounded model checking and generating SMT benchmarks. More recently we also successfully applied SmacC for high-level timing analysis of programs to infer exact loop bounds and safe over-approximations. SmacC uses the logic for bit-vectors with arrays to construct a bit-precise memory-model of a program for path-wise exploration.
|
|
| 2. |
- Biere, Armin, et al.
(författare)
-
The Auspicious Couple: Symbolic Execution and WCET Analysis
- 2013
-
Ingår i: OpenAccess Series in Informatics. - 2190-6807. - 9783939897545 ; 30, s. 53-63
-
Konferensbidrag (refereegranskat)abstract
- We have recently shown that symbolic execution together with the implicit path enumeration technique can successfully be applied in the Worst-Case Execution Time (WCET) analysis of programs. Symbolic execution offers a precise framework for program analysis and tracks complex program properties by analyzing single program paths in isolation. This path-wise program exploration of symbolic execution is, however, computationally expensive, which often prevents full symbolic analysis of larger applications: the number of paths in a program increases exponentially with the number of conditionals, a situation denoted as the path explosion problem. Therefore, for applying symbolic execution in the timing analysis of programs, we propose to use WCET analysis as a guidance for symbolic execution in order to avoid full symbolic coverage of the program. By focusing only on paths or program fragments that are relevant for WCET analysis, we keep the computational costs of symbolic execution low. Our WCET analysis also profits from the precise results derived via symbolic execution. In this article we describe how use-cases of symbolic execution are materialized in the r-TuBound toolchain and present new applications of WCET-guided symbolic execution for WCET analysis. The new applications of selective symbolic execution are based on reducing the effort of symbolic analysis by focusing only on relevant program fragments. By using partial symbolic program coverage obtained by selective symbolic execution, we improve the WCET analysis and keep the effort for symbolic execution low.
|
|
| 3. |
- Knoop, Jens, et al.
(författare)
-
Replacing Conjectures by Positive Knowledge: Inferring Proven Precise Worst-Case Execution Time Bounds Using Symbolic Execution
- 2017
-
Ingår i: Journal of Symbolic Computation. - : Elsevier BV. - 1095-855X .- 0747-7171. ; 80, s. 101-124
-
Tidskriftsartikel (refereegranskat)abstract
- 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.
|
|
| 4. |
- Knoop, Jens, et al.
(författare)
-
WCET Squeezing: On-Demand Feasibility Refinement for Proven Precise WCET-Bounds
- 2013
-
Ingår i: Proceedings of the 21st International Conference on Real-Time Networks and Systems (RTNS 2013), October 17-18, 2013, Sophia Antipolis, France. Michel Auguin and Robert de Simone and Robert Davis and Emmanuel Grolleau (editors), ACM. - New York, NY, USA : ACM. - 9781450320580 ; , s. 161-170
-
Konferensbidrag (refereegranskat)abstract
- The Worst-Case Execution Time (WCET) computed by a WCET analyzer is usually not tight, leaving a gap between the actual and the computed WCET of a program. In this article we present a novel on-demand WCET feasibility refinement technique, called WCET Squeezing, for minimizing this gap.WCET Squeezing provides conceptually new means for addressing the classical problem of WCET computation, by deriving a WCET bound that comes as close as possible to the actual one. WCET Squeezing is an anytime algorithm, that is, it can be stopped at any time without violating the soundness of its results. This anytime property allows to apply WCET Squeezing not only for deriving precise WCET bounds but to also prove additional timing constraints over the program. Namely, WCET Squeezing can be used to guarantee that a program is fast enough by ensuring that the WCET of the program is below some required limit. If the initially computed WCET of the program is above this limit, WCET Squeezing can be stopped as soon as the squeezed WCET of the program is below the limit (proving the program meets the required timing constraint), or if the squeezed WCET is tight but above the given limit (proving the program cannot meet the timing constraint). WCET Squeezing can also be used until a given time budget is exhausted to compute a tight(er) WCET bound for a program. These new applications of WCET Squeezing are out of the scope of traditional WCET analyzers.WCET Squeezing combines symbolic program execution with the Implicit Path Enumeration Technique (IPET) for computing a precise WCET bound. WCET Squeezing is applicable as a post-process to any WCET analyzer which encodes the IPET problem as an Integer Linear Program (ILP). We implemented our method in the r-TuBound toolchain and evaluated our implementation on a set examples taken from the Mälardalen WCET benchmark suite. Our experiments demonstrate that WCET Squeezing can significantly tighten the WCET bounds of programs. Moreover, the derived WCET bounds are proven to be precise at a moderate computational cost.
|
|
| 5. |
- Lisper, Björn, et al.
(författare)
-
Practical Experiences of Applying Source-Level WCET Flow Analysis on Industrial Code
- 2010
-
Ingår i: Lecture Notes in Computer Science, vol. 6416. - Berlin, Heidelberg : Springer. - 9783642165603 ; , s. 449-463
-
Bokkapitel (refereegranskat)abstract
- Code-level timing analysis, such as Worst-Case Execution Time (WCET) analysis, takes place at the binary level. However, much information that is important for the analysis, such as constraints on possible program flows, are easier to derive at the source code level since this code contains much more information. Therefore, different source-level analyses can provide valuable support for timing analysis However, source-level analysis is not always smoothly applicable in industrial projects. In this paper we report on the experiences of applying source-level analysis to industrial code in the ALL-TIMES FP7 project: the promises, the pitfalls, and the workarounds that were developed. We also discuss various approaches to how the difficulties that were encountered can be tackled.
|
|
| 6. |
- Lisper, Björn, et al.
(författare)
-
Practical experiences of applying source-level WCET flow analysis to industrial code
- 2013
-
Ingår i: International Journal on Software Tools for Technology Transfer. - : Springer Science and Business Media LLC. - 1433-2779 .- 1433-2787. ; 15:1, s. 53-63
-
Tidskriftsartikel (refereegranskat)abstract
- Code-level timing analysis, such as worst-case execution time (WCET) analysis, usually takes place at the binary level. However, many program properties that are important for the analysis, such as constraints on possible program flows, are easier to derive at the source code level since this code contains much more information. Therefore, various source-level analyses can provide valuable support for timing analysis. However, source-level analysis is not always smoothly applicable in industrial settings. In this paper, we report on the experiences of applying source-level analysis to industrial code in the ALL-TIMES project: the promises, the pitfalls, and the workarounds that were developed. We also discuss various approaches to how the difficulties that were encountered can be tackled.
|
|
| 7. |
|
|
