Towards energy consumption verification via static analysis

López García, Pedro and Haemmerlé, Remy and Klemen, Maximiliano and Liqat, Umer and Hermenegildo, Manuel V. (2016). Towards energy consumption verification via static analysis. In: "Workshop on High Performance Energy Efficient Embedded Systems (HIP3ES) 2015", 21 Jan 2015, Amsterdam, Holanda.

Description

Title: Towards energy consumption verification via static analysis
Author/s:
  • López García, Pedro
  • Haemmerlé, Remy
  • Klemen, Maximiliano
  • Liqat, Umer
  • Hermenegildo, Manuel V.
Item Type: Presentation at Congress or Conference (Article)
Event Title: Workshop on High Performance Energy Efficient Embedded Systems (HIP3ES) 2015
Event Dates: 21 Jan 2015
Event Location: Amsterdam, Holanda
Title of Book: Proceedings of the Workshop on High Performance Energy Efficient Embedded Systems (HIP3ES) 2015
Date: 2016
Subjects:
Freetext Keywords: Energy consumption analysis and verification; Resource usage analysis and verification; Static analysis; Verification
Faculty: E.T.S. de Ingenieros Informáticos (UPM)
Department: Lenguajes y Sistemas Informáticos e Ingeniería del Software
Creative Commons Licenses: Recognition - No derivative works - Non commercial

Full text

[img]
Preview
PDF - Requires a PDF viewer, such as GSview, Xpdf or Adobe Acrobat Reader
Download (447kB) | Preview

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.

More information

Item ID: 52631
DC Identifier: http://oa.upm.es/52631/
OAI Identifier: oai:oa.upm.es:52631
Official URL: https://arxiv.org/abs/1512.09369v1
Deposited by: Biblioteca Facultad de Informatica
Deposited on: 15 Oct 2018 12:08
Last Modified: 15 Oct 2018 12:12
  • Logo InvestigaM (UPM)
  • Logo GEOUP4
  • Logo Open Access
  • Open Access
  • Logo Sherpa/Romeo
    Check whether the anglo-saxon journal in which you have published an article allows you to also publish it under open access.
  • Logo Dulcinea
    Check whether the spanish journal in which you have published an article allows you to also publish it under open access.
  • Logo de Recolecta
  • Logo del Observatorio I+D+i UPM
  • Logo de OpenCourseWare UPM