Quantitative Analysis of Embedded Software Using Game-Theoretic Learning

摘要

The analysis of quantitative properties, such as timing and power, is central to the design of reliable real-time embedded software and systems. However, the verification of such properties on a program is made difficult by their heavy dependence on the program's environment, such as the processor it runs on. Modeling the environment by hand can be tedious, error-prone, and time consuming. In this paper, we present a new, game-theoretic approach to analyzing quantitative properties that is based on performing systematic measurements to automatically learn a model of the environment. We model the estimation problem as a game between our algorithm (player) and the environment of the program (adversary) where the player seeks to accurately predict program properties while the adversary sets environment parameters to thwart the player. We present both theoretical and experimental evidence for the utility of our game-theoretic approach. On the theoretical side, we show that we can predict the program property for all execution paths with probability greater than 1 - delta by only making a number of measurements that is polynomial in ln(1/delta) and the program size. Experimental results for execution time analysis demonstrate that our approach is efficient, effective, and highly portable.