Please use this identifier to cite or link to this item: https://doi.org/10.1007/s11241-013-9178-0
Title: Scalable and precise refinement of cache timing analysis via path-sensitive verification
Authors: Chattopadhyay, S.
Roychoudhury, A. 
Keywords: Abstract interpretation
Constraint solving
Model checking
WCET analysis
Issue Date: Jul-2013
Citation: Chattopadhyay, S., Roychoudhury, A. (2013-07). Scalable and precise refinement of cache timing analysis via path-sensitive verification. Real-Time Systems 49 (4) : 517-562. ScholarBank@NUS Repository. https://doi.org/10.1007/s11241-013-9178-0
Abstract: Hard real-time systems require absolute guarantees in their execution times. Worst case execution time (WCET) of a program has therefore become an important problem to address. However, performance enhancing features of a processor (e.g. cache) make WCET analysis a difficult problem. In this paper, we propose a novel analysis framework by combining abstract interpretation and program verification for different varieties of cache analysis ranging from single to multi-core platforms. Our framework can be instantiated with different program verification techniques, such as model checking and symbolic execution. Our modeling is used to develop a precise yet scalable timing analysis method on top of the Chronos WCET analysis tool. Experimental results demonstrate that we can obtain significant improvement in precision with reasonable analysis time overhead. © 2013 Springer Science+Business Media New York.
Source Title: Real-Time Systems
URI: http://scholarbank.nus.edu.sg/handle/10635/78331
ISSN: 09226443
DOI: 10.1007/s11241-013-9178-0
Appears in Collections:Staff Publications

Show full item record
Files in This Item:
There are no files associated with this item.

SCOPUSTM   
Citations

13
checked on Dec 12, 2018

WEB OF SCIENCETM
Citations

7
checked on Dec 4, 2018

Page view(s)

41
checked on Oct 27, 2018

Google ScholarTM

Check

Altmetric


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.