关键词：时序分析；基准路径；内部实施和评估
摘 要：Timing analysis is central to the design and implementation of cyber-physical systems. This thesis presents GameTime, a timing analysis toolkit that is based on a combination of game-theoretic online learning and systematic testing using satis ability modulo theories (SMT) solvers. GameTime can be used to tackle a range of problems related to program timing, including estimating the worst-case execution time, predicting the distribution of execution times, and detecting timing-related anomalies.This thesis describes the details of the implementation of GameTime. The notion of basis paths is used to handle the exponentially many paths in a program. The issues that arise during the translation of statements in C programs to the equivalent clauses in SMT queries are presented, and the techniques used by GameTime to address these issues are elaborated through examples. Finally, experimental results demonstrate the speed of GameTime analysis and the accuracy of the predictions made by GameTime, with a relative error margin of less than 5% on most of the benchmarks measured.