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

SeriesACM International Conference Proceeding Series

Conference

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

    Fingerprint

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. ACM International Conference Proceeding Series https://doi.org/10.1145/3191697.3213805