Interval-based Resource Usage Verification by Translation into Horn Clauses and an Application to Energy Consumption

TL;DR

This paper introduces a flexible static resource usage verification framework that infers and compares resource functions against specifications, supporting multiple languages and data-dependent bounds, with an application to energy consumption in embedded programs.

Contribution

It extends existing frameworks to handle interval-based specifications, supports various input languages through Horn clause translation, and applies to energy verification in embedded systems.

Findings

Successfully implemented within Ciao/CiaoPP framework.

Extended class of functions for resource analysis.

Validated on energy consumption specifications for embedded programs.

Abstract

Many applications require conformance with specifications that constrain the use of resources, such as execution time, energy, bandwidth, etc. We have presented a configurable framework for static resource usage verification where specifications can include lower and upper bound, data size-dependent resource usage functions. To statically check such specifications, our framework infers the same type of resource usage functions, which safely approximate the actual resource usage of the program, and compares them against the specification. We review how this framework supports several languages and compilation output formats by translating them to an intermediate representation based on Horn clauses and using the configurability of the framework to describe the resource semantics of the input language. We provide a more detailed formalization and extend the framework so that both resource usage specification and analysis/verification output can include preconditions expressing intervals for the input data sizes for which assertions are applicable, proved, or disproved. Most importantly, we also extend the classes of functions that can be checked. We provide results from an implementation within the Ciao/CiaoPP framework, and report on a tool built by instantiating this framework for the verification of energy consumption specifications for imperative/embedded programs. This paper is under consideration for publication in Theory and Practice of Logic Programming (TPLP).