基于程序切片和实时的模型检验的WCET计算
Computation of WCET using Program Slicing and Real-Time Model-Checking
摘要：
在现代复杂体系结构上计算精确的WCET是一项具有挑战性的任务。在过去的十年里，这个问题已经引起了很多关注，但仍然存在一些悬而未决的问题。首先，需要二进制程序的控制流图（CFG）来计算WCET，并且使用生成二进制代码的编译器的一些内部知识来构建此CFG;此外，一旦构建了CFG，就必须手动注释循环边界。其次，计算WCET的算法（结合了抽象解释和线性规划）是为特定的架构量身定制的：改变架构（例如用ARM9替换ARM 7）需要设计一个新的自组织算法。第三，计算结果（使用可用的工具获得）的紧密性没有与在真实硬件上测量的实际执行时间进行比较。在本文中，我们解决上述问题。我们首先描述了一个全自动的方法来计算一个CFG完全基于二进制程序进行分析。其次，我们将硬件的模型描述为时间自动机的产物，并且该模型独立于程序描述。在硬件上运行的程序的模型是通过将程序（的自动机）与硬件的（时间自动机）模型同步来获得的。计算WCET减少到一个可达性问题的同步模型和解决使用模型检查UPPAAL。最后，我们提出了一个严格的方法，使我们能够比较我们的计算结果，在一个真正的平台，ARM920 T上测量的实际执行时间。
英文摘要：
Computing accurate WCET on modern complex architectures is a challenging task. This problem has been devoted a lot of attention in the last decade but there are still some open issues. First, the control flow graph (CFG) of a binary program is needed to compute the WCET and this CFG is built using some internal knowledge of the compiler that generated the binary code; moreover once constructed the CFG has to be manually annotated with loop bounds. Second, the algorithms to compute the WCET (combining Abstract Interpretation and Integer Linear Programming) are tailored for specific architectures: changing the architecture (e.g. replacing an ARM7 by an ARM9) requires the design of a new ad hoc algorithm. Third, the tightness of the computed results (obtained using the available tools) are not compared to actual execution times measured on the real hardware. In this paper we address the above mentioned problems. We first describe a fully automatic method to compute a CFG based solely on the binary program to analyse. Second, we describe the model of the hardware as a product of timed automata, and this model is independent from the program description. The model of a program running on a hardware is obtained by synchronizing (the automaton of) the program with the (timed automata) model of the hardware. Computing the WCET is reduced to a reachability problem on the synchronised model and solved using the model-checker UPPAAL. Finally, we present a rigorous methodology that enables us to compare our computed results to actual execution times measured on a real platform, the ARM920T.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
