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.
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.