Quantitative Analysis of Systems Using Game-Theoretic Learning

Sanjit A. Seshia and Alexander Rakhlin. Quantitative Analysis of Systems Using Game-Theoretic Learning. ACM Transactions on Embedded Computing Systems (TECS), 11(S2):55:1–55:27, 2012.

Download

[pdf] 

Abstract

The analysis of quantitative properties, such as timing and power, is central to the design ofreliable embedded software and systems. However, the verification of such properties on a programis made difficult by their heavy dependence on the program’s environment, such as the processor itruns on. Modeling the environment by hand can be tedious, error-prone and time consuming. Inthis paper, we present a new, game-theoretic approach to analyzing quantitative properties that isbased 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 theprogram (adversary), where the player seeks to accurately predict the property of interest while theadversary sets environment states and parameters. To solve this problem, we employ a randomizedstrategy that repeatedly tests the program along a linear-sized set of program paths called basispaths, using the resulting measurements to infer a weighted-graph model of the environment,from which quantitative properties can be predicted. Test cases are automatically generatedusing satisfiability modulo theories (SMT) solving. We prove that our algorithm can, undercertain assumptions and with arbitrarily high probability, accurately predict properties such asworst-case execution time or estimate the distribution of execution times. Experimental results forexecution time analysis demonstrate that our approach is efficient, accurate, and highly portable.

BibTeX

@Article{seshia-acmtecs10,
  author = 	 {Sanjit A. Seshia and Alexander Rakhlin},
  title = 	 {Quantitative Analysis of Systems Using Game-Theoretic Learning},
  journal = 	 {ACM Transactions on Embedded Computing Systems (TECS)},
  year = 	 {2012},
  OPTkey = 	 {},
  volume = 	 {11},
  number = 	 {S2},
  pages = 	 {55:1--55:27},
  OPTmonth = 	 {},
  OPTnote = 	 {Accepted 2010.},
  OPTannote = 	 {},
  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.
  },
}