Trickle: automated infeasible path detection using all minimal unsatisfiable subsets

Select |




Print


Blackham, Bernard; Liffiton, Mark; Heiser, Gernot

Blackham, Bernard; Liffiton, Mark; Heiser, Gernot


2014-04-15


Conference Material


Real Time and Embedded Technology Applications Symposium


Berlin, Germany


169-178


Static analysis techniques can be used to compute safe bounds on the worst-case execution time (WCET) of programs. For large programs, abstractions are often required in order to curb computational complexity. These abstractions may introduce infeasible paths which result in significant overestimation. These paths can be eliminated by adding additional constraints to the static analysis. Such constraints can be found manually but this is labour-intensive and error-prone. Automated methods of finding infeasible path constraints are thus highly desirable. In this paper we present Trickle: a method to automatically detect infeasible paths on compiled binary programs, in order to refine WCET estimates. We build upon the Sequoll framework and apply satisfiability modulo theory (SMT) solvers to find classes of infeasible paths. Unlike other techniques, Trickle can find infeasible paths which contain an arbitrary number of conflicting conditions. We also integrate the compute all minimal unsatisfiable subsets (CAMUS) algorithm to reduce the number of refinement iterations required. We show the practicality of Trickle by applying it to a WCET analysis of the seL4 microkernel. We also evaluate its effectiveness on the Mälardalen WCET benchmarks.


worst-case execution time, real-time systems


http://2014.rtas.org/


978-1-4799-4691-4


nicta:7526


Blackham, Bernard; Liffiton, Mark; Heiser, Gernot. Trickle: automated infeasible path detection using all minimal unsatisfiable subsets. In: Richard West Editor, editor/s. Real Time and Embedded Technology Applications Symposium; Berlin, Germany. 2014-04-15. 169-178.



Loading citation data...

Citation counts
(Requires subscription to view)