Scalable Timing Analysis with Refinement

Abstract. Traditional timing analysis techniques rely on composing system-level worst-case behavior with local worst-case behaviors of indi-vidual components. In many complex real-time systems, no single local worst-case behavior exists for each component and it generally requires to enumerate all the combinations of individual local behaviors to find the global worst case. This paper presents a scalable timing analysis tech-nique based on abstraction refinement, which provides effective guidance to significantly prune away state space and quickly verify the desired tim-ing properties. We first establish the general framework of the method, and then apply it to solve the analysis problem for several different real-time task models