Sanjit A. Seshia and Alexander Rakhlin

EECS Department, University of California, Berkeley

Technical Report No. UCB/EECS-2009-130

September 22, 2009

http://www2.eecs.berkeley.edu/Pubs/TechRpts/2009/EECS-2009-130.pdf

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−d by only making a number of measurements that is polynomial in ln(1/d) and the program size. Experimental results for execution time analysis demonstrate that our approach is efficient, effective, and highly portable.

---

BibTeX citation:

@techreport{Seshia:EECS-2009-130,
    Author= {Seshia, Sanjit A. and Rakhlin, Alexander},
    Title= {Quantitative Analysis of Embedded Software Using Game-Theoretic Learning},
    Year= {2009},
    Month= {Sep},
    Url= {http://www2.eecs.berkeley.edu/Pubs/TechRpts/2009/EECS-2009-130.html},
    Number= {UCB/EECS-2009-130},
    Abstract= {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−d by only making a number of measurements
that is polynomial in ln(1/d) and the program size. Experimental results for execution time analysis
demonstrate that our approach is efficient, effective, and highly portable.},
}

EndNote citation:

%0 Report
%A Seshia, Sanjit A. 
%A Rakhlin, Alexander 
%T Quantitative Analysis of Embedded Software Using Game-Theoretic Learning
%I EECS Department, University of California, Berkeley
%D 2009
%8 September 22
%@ UCB/EECS-2009-130
%U http://www2.eecs.berkeley.edu/Pubs/TechRpts/2009/EECS-2009-130.html
%F Seshia:EECS-2009-130