TY - GEN
T1 - TIC
T2 - 17th ACM SIGPLAN/SIGBED Conference on Languages, Compilers, Tools and Theory for Embedded Systems, LCTES 2016
AU - Metta, Ravindra
AU - Becker, Martin
AU - Bokil, Prasad
AU - Chakraborty, Samarjit
AU - Venkatesh, R.
N1 - Publisher Copyright:
©2016 ACM.
PY - 2016/6/13
Y1 - 2016/6/13
N2 - The application of Model Checking to compute WCET has not been explored as much as Integer Linear Programming (ILP), primarily because model checkers fail to scale for complex programs. These programs have loops with large or unknown bounds, leading to a state space explosion that model checkers cannot handle. To overcome this, we have developed a technique, TIC, that employs slicing, loop acceleration and over-approximation on timeannotated source code, enabling Model Checking to scale better for WCET computation. Further, our approach is parametric, so that the user can make a trade-off between the tightness of WCET estimate and the analysis time. We conducted experiments on the Mälardalen benchmarks to evaluate the effect of various abstractions on the WCET estimate and analysis time. Additionally, we compared our estimates to those made by an ILP-based analyzer and found that ours were tighter for more than 30% of the examples and equal for the rest.
AB - The application of Model Checking to compute WCET has not been explored as much as Integer Linear Programming (ILP), primarily because model checkers fail to scale for complex programs. These programs have loops with large or unknown bounds, leading to a state space explosion that model checkers cannot handle. To overcome this, we have developed a technique, TIC, that employs slicing, loop acceleration and over-approximation on timeannotated source code, enabling Model Checking to scale better for WCET computation. Further, our approach is parametric, so that the user can make a trade-off between the tightness of WCET estimate and the analysis time. We conducted experiments on the Mälardalen benchmarks to evaluate the effect of various abstractions on the WCET estimate and analysis time. Additionally, we compared our estimates to those made by an ILP-based analyzer and found that ours were tighter for more than 30% of the examples and equal for the rest.
KW - ANSI-C
KW - Model checking
KW - Worst-Case execution time
UR - http://www.scopus.com/inward/record.url?scp=84978063259&partnerID=8YFLogxK
U2 - 10.1145/2907950.2907961
DO - 10.1145/2907950.2907961
M3 - Conference contribution
AN - SCOPUS:84978063259
T3 - Proceedings of the ACM SIGPLAN Conference on Languages, Compilers, and Tools for Embedded Systems (LCTES)
SP - 72
EP - 81
BT - LCTES 2016 - Proceedings of the 17th ACM SIGPLAN/SIGBED Conference on Languages, Compilers, Tools, and Theory for Embedded Systems, co-located with PLDI 2016
A2 - Whalley, David B.
A2 - Kuo, Tei-Wei
PB - Association for Computing Machinery
Y2 - 13 June 2016 through 14 June 2016
ER -