Sanjit A. Seshia and Alexander Rakhlin

EECS Department, University of California, Berkeley

Technical Report No. UCB/EECS-2010-102

June 30, 2010

http://www2.eecs.berkeley.edu/Pubs/TechRpts/2010/EECS-2010-102.pdf

The analysis of quantitative properties, such as timing and power, is central to the design of reliable 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 problem as a game between our algorithm (player) and the environment of the program (adversary), where the player seeks to accurately predict the property of interest while the adversary sets environment states and parameters. To solve this problem, we employ a randomized strategy that repeatedly tests the program along a linear-sized set of program paths called basis paths, using the resulting measurements to infer a weighted-graph model of the environment, from which quantitative properties can be predicted. Test cases are automatically generated using satisfiability modulo theories (SMT) solving. We prove that our algorithm can, under certain assumptions and with arbitrarily high probability, accurately predict properties such as worst-case execution time or estimate the distribution of execution times. Experimental results for execution time analysis demonstrate that our approach is efficient, accurate, and highly portable.

---

BibTeX citation:

@techreport{Seshia:EECS-2010-102,
    Author= {Seshia, Sanjit A. and Rakhlin, Alexander},
    Title= {Quantitative Analysis of Systems Using Game-Theoretic Learning},
    Year= {2010},
    Month= {Jun},
    Url= {http://www2.eecs.berkeley.edu/Pubs/TechRpts/2010/EECS-2010-102.html},
    Number= {UCB/EECS-2010-102},
    Abstract= {The analysis of quantitative properties, such as timing and power,
is central to the design of reliable 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 problem as a game between our algorithm 
(player) and the environment of the program (adversary), where the player 
seeks to accurately predict the property of interest while the adversary sets 
environment states and parameters.
To solve this problem,
we employ a randomized strategy that repeatedly tests the program
along a linear-sized set of program paths called basis paths, using 
the resulting measurements to infer a weighted-graph model of the environment,
from which quantitative properties can be predicted.
Test cases are automatically generated using satisfiability modulo theories (SMT) solving.
We prove that our algorithm can, under certain assumptions and with arbitrarily
high probability, accurately 
predict properties such as worst-case execution time or estimate the distribution
of execution times.
Experimental results for execution time analysis demonstrate that our 
approach is efficient, accurate, and highly portable.},
}

EndNote citation:

%0 Report
%A Seshia, Sanjit A. 
%A Rakhlin, Alexander 
%T Quantitative Analysis of Systems Using Game-Theoretic Learning
%I EECS Department, University of California, Berkeley
%D 2010
%8 June 30
%@ UCB/EECS-2010-102
%U http://www2.eecs.berkeley.edu/Pubs/TechRpts/2010/EECS-2010-102.html
%F Seshia:EECS-2010-102