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.

Google ScholarTM

Check

Altmetric


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