Scalable and Precise Refinement of Cache Timing Analysis via Model Checking
- 1 November 2011
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- p. 193-203
- https://doi.org/10.1109/rtss.2011.25
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 approach of combining abstract interpretation and model checking for different varieties of cache analysis ranging from single to multi-core platforms. 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.Keywords
This publication has 13 references indexed in Scilit:
- Scope-Aware Data Cache Analysis for WCET EstimationPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2011
- Combining Abstract Interpretation with Model Checking for Timing Analysis of Multicore SoftwarePublished by Institute of Electrical and Electronics Engineers (IEEE) ,2010
- Resilience analysisPublished by Association for Computing Machinery (ACM) ,2010
- Timing Analysis of Concurrent Programs Running on Shared Cache Multi-CoresPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2009
- A New Notion of Useful Cache Block to Improve the Bounds of Cache-Related Preemption DelayPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2009
- Performance debugging of Esterel specificationsPublished by Association for Computing Machinery (ACM) ,2008
- WCET Analysis for Multi-Core Processors with Shared L2 Instruction CachesPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2008
- Chronos: A timing analyzer for embedded softwareScience of Computer Programming, 2007
- Bounded Model Checking Using Satisfiability SolvingFormal Methods in System Design, 2001
- Analysis of cache-related preemption delay in fixed-priority preemptive schedulingIEEE Transactions on Computers, 1998