Detecting energy bugs and hotspots in control software using model checking

Research output: Chapter in Book/Report/Conference proceedingConference article in proceedingAcademicpeer-review

Abstract

We explore a way to find energy deficiencies in code by model checking, both properties related to utilisation (energy hotspots) and not related to utilisation (energy bugs). Temporal logic properties (expressed using LTL) finds these deficiencies during the development of a system, employing a novel energy-inefficiency metric. The formal model is deduced from hardware specifications, a definition of utilisation and a control software application written in C. Model checking results in a set of traces (formally a counter-example) that can be related to the matching execution path in the source code by the software developer. The traces include energy footprints and enable developers to improve the energy efficiency of the application. A smart light system serves as a case study to evaluate the proposed approach.
Original languageEnglish
Title of host publicationProgramming'18 Companion Conference Companion of the 2nd International Conference on Art, Science, and Engineering of Programming
Place of PublicationNew York, NY
Publisheracm
Chapter22
Pages93-98
Number of pages6
ISBN (Print)9781450355131
DOIs
Publication statusPublished - 2018
EventProgramming 2018 Companion: Conference Companion of the 2nd International Conference on Art, Science, and Engineering of Programming - Nice, France
Duration: 9 Apr 201812 Apr 2018
https://2018.programmingconference.org/home

Publication series

NameACM International Conference Proceeding Series

Conference

ConferenceProgramming 2018 Companion
CountryFrance
CityNice
Period9/04/1812/04/18
Internet address

Fingerprint

Model checking
Energy utilization
Temporal logic
Application programs
Energy efficiency
Specifications
Hardware

Cite this

Gastel, P. V., Gastel, B. V., & Eekelen, M. C. J. D. V. (2018). Detecting energy bugs and hotspots in control software using model checking. In Programming'18 Companion Conference Companion of the 2nd International Conference on Art, Science, and Engineering of Programming (pp. 93-98). (ACM International Conference Proceeding Series). New York, NY: acm. https://doi.org/10.1145/3191697.3213805
Gastel, Pascal van ; Gastel, Bernard van ; Eekelen, Marko C. J. D. van. / Detecting energy bugs and hotspots in control software using model checking. Programming'18 Companion Conference Companion of the 2nd International Conference on Art, Science, and Engineering of Programming. New York, NY : acm, 2018. pp. 93-98 (ACM International Conference Proceeding Series).
@inproceedings{dc3a2de8a6424d3d9e62f1f69ef16aec,
title = "Detecting energy bugs and hotspots in control software using model checking",
abstract = "We explore a way to find energy deficiencies in code by model checking, both properties related to utilisation (energy hotspots) and not related to utilisation (energy bugs). Temporal logic properties (expressed using LTL) finds these deficiencies during the development of a system, employing a novel energy-inefficiency metric. The formal model is deduced from hardware specifications, a definition of utilisation and a control software application written in C. Model checking results in a set of traces (formally a counter-example) that can be related to the matching execution path in the source code by the software developer. The traces include energy footprints and enable developers to improve the energy efficiency of the application. A smart light system serves as a case study to evaluate the proposed approach.",
author = "Gastel, {Pascal van} and Gastel, {Bernard van} and Eekelen, {Marko C. J. D. van}",
year = "2018",
doi = "10.1145/3191697.3213805",
language = "English",
isbn = "9781450355131",
series = "ACM International Conference Proceeding Series",
publisher = "acm",
pages = "93--98",
booktitle = "Programming'18 Companion Conference Companion of the 2nd International Conference on Art, Science, and Engineering of Programming",

}

Gastel, PV, Gastel, BV & Eekelen, MCJDV 2018, Detecting energy bugs and hotspots in control software using model checking. in Programming'18 Companion Conference Companion of the 2nd International Conference on Art, Science, and Engineering of Programming. ACM International Conference Proceeding Series, acm, New York, NY, pp. 93-98, Programming 2018 Companion, Nice, France, 9/04/18. https://doi.org/10.1145/3191697.3213805

Detecting energy bugs and hotspots in control software using model checking. / Gastel, Pascal van; Gastel, Bernard van; Eekelen, Marko C. J. D. van.

Programming'18 Companion Conference Companion of the 2nd International Conference on Art, Science, and Engineering of Programming. New York, NY : acm, 2018. p. 93-98 (ACM International Conference Proceeding Series).

Research output: Chapter in Book/Report/Conference proceedingConference article in proceedingAcademicpeer-review

TY - GEN

T1 - Detecting energy bugs and hotspots in control software using model checking

AU - Gastel, Pascal van

AU - Gastel, Bernard van

AU - Eekelen, Marko C. J. D. van

PY - 2018

Y1 - 2018

N2 - We explore a way to find energy deficiencies in code by model checking, both properties related to utilisation (energy hotspots) and not related to utilisation (energy bugs). Temporal logic properties (expressed using LTL) finds these deficiencies during the development of a system, employing a novel energy-inefficiency metric. The formal model is deduced from hardware specifications, a definition of utilisation and a control software application written in C. Model checking results in a set of traces (formally a counter-example) that can be related to the matching execution path in the source code by the software developer. The traces include energy footprints and enable developers to improve the energy efficiency of the application. A smart light system serves as a case study to evaluate the proposed approach.

AB - We explore a way to find energy deficiencies in code by model checking, both properties related to utilisation (energy hotspots) and not related to utilisation (energy bugs). Temporal logic properties (expressed using LTL) finds these deficiencies during the development of a system, employing a novel energy-inefficiency metric. The formal model is deduced from hardware specifications, a definition of utilisation and a control software application written in C. Model checking results in a set of traces (formally a counter-example) that can be related to the matching execution path in the source code by the software developer. The traces include energy footprints and enable developers to improve the energy efficiency of the application. A smart light system serves as a case study to evaluate the proposed approach.

U2 - 10.1145/3191697.3213805

DO - 10.1145/3191697.3213805

M3 - Conference article in proceeding

SN - 9781450355131

T3 - ACM International Conference Proceeding Series

SP - 93

EP - 98

BT - Programming'18 Companion Conference Companion of the 2nd International Conference on Art, Science, and Engineering of Programming

PB - acm

CY - New York, NY

ER -

Gastel PV, Gastel BV, Eekelen MCJDV. Detecting energy bugs and hotspots in control software using model checking. In Programming'18 Companion Conference Companion of the 2nd International Conference on Art, Science, and Engineering of Programming. New York, NY: acm. 2018. p. 93-98. (ACM International Conference Proceeding Series). https://doi.org/10.1145/3191697.3213805