Paper Info
Title
Trickle: Automated infeasible path detection using all minimal unsatisfiable subsets
Abstract
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 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.
Year
DOI
Venue
2014
10.1109/RTAS.2014.6926000
RTAS
Keywords
Field
DocType
compute all minimal unsatisfiable subsets,software verification and validation,wcet,worst-case execution time,automated infeasible path detection,trickle,static analysis technique,computational complexity,computability,real time systems,operating system kernels,smt solver,sequoll framework,program diagnostics,camus algorithm,satisfiability modulo theory,mathematical model,hardware,algorithm design and analysis,worst case execution time
Algorithm design,Computer science,Modulo,Static analysis,Satisfiability,Microkernel,Algorithm,Real-time computing,Computational complexity theory,Binary number,TRICKLE
Conference
ISSN
Citations 
PageRank 
1080-1812
11
0.58
References 
Authors
22
3
Name
Order
Citations
PageRank
Bernard Blackham1694.41
Mark H. Liffiton2110.58
Gernot Heiser32525137.42