SMT-Based Timing Analysis and Verification of Real-Time Task

Timing analysis plays an important role in embedded real-time system design. And the cache hit/miss behavior analysis is a key problem in timing analysis, especially difficult in the sharing caches among multiple cores. The combination of Abstraction Interpretation (AI) and Satisfiability Modulo Theories (SMT) methods are used in timing analysis. SMT based on the rigorous first-order logic has both computational and analytical capabilities, thus the usage of SMT in timing analysis can more effectively relieve the pressure of AI. However, the existing methods do not solve the problem of behavior analysis of shared instruction caches, and do not complete the computation of upper bounds on the execution time of tasks. In this paper, we adopt AI to complete the refined hit/miss classification of instructions accessing the shared instruction cache, employ SMT to complete the difficult work of behavior analysis of shared instruction cache, and explore an iteration optimization algorithm of logarithmic order to compute the results. From the experiments, our approach can accurately predict the upper bounds on the execution time.