Towards energy consumption verification via static analysis

Abstract

In this paper we leverage an existing general framework
for resource usage verification and specialize it for verifying
energy consumption specifications of embedded programs.
Such specifications can include both lower and upper bounds
on energy usage, and they can express intervals within which
energy usage is to be certified to be within such bounds.
The bounds of the intervals can be given in general as functions
on input data sizes. Our verification system can prove
whether such energy usage specifications are met or not.
It can also infer the particular conditions under which the
specifications hold. To this end, these conditions are also
expressed as intervals of functions of input data sizes, such
that a given specification can be proved for some intervals
but disproved for others. The specifications themselves can
also include preconditions expressing intervals for input data
sizes. We report on a prototype implementation of our approach
within the CiaoPP system for the XC language and
XS1-L architecture, and illustrate with an example how embedded
software developers can use this tool, and in particular
for determining values for program parameters that
ensure meeting a given energy budget while minimizing the
loss in quality of service.