Detecting energy bugs and hotspots in control software using model checking

Pascal van Gastel; Bernard van Gastel; Marko C. J. D. van Eekelen

doi:10.1145/3191697.3213805

Detecting energy bugs and hotspots in control software using model checking

Pascal van Gastel, Bernard van Gastel, Marko C. J. D. van Eekelen

Research Line Resilience (part of LIRS program)

Research output: Chapter in Book/Report/Conference proceeding › Conference Article in proceeding › Academic › peer-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 language	English
Title of host publication	Programming 2018 Companion - Conference Companion of the 2nd International Conference on Art, Science, and Engineering of Programming
Editors	Jennifer B. Sartor, Stefan Marr
Place of Publication	New York, NY
Publisher	acm
Chapter	22
Pages	93-98
Number of pages	6
ISBN (Print)	9781450355131
DOIs	https://doi.org/10.1145/3191697.3213805
Publication status	Published - 9 Apr 2018
Event	Programming 2018 Companion: Conference Companion of the 2nd International Conference on Art, Science, and Engineering of Programming - Nice, France Duration: 9 Apr 2018 → 12 Apr 2018 https://2018.programmingconference.org/home

Publication series

Series	ACM International Conference Proceeding Series

Conference

Conference	Programming 2018 Companion
Country/Territory	France
City	Nice
Period	9/04/18 → 12/04/18
Internet address	https://2018.programmingconference.org/home

Keywords

Energy consumption analysis
Model checking

Access to Document

10.1145/3191697.3213805

Cite this

Gastel, Pascal van ; Gastel, Bernard van ; Eekelen, Marko C. J. D. van. / Detecting energy bugs and hotspots in control software using model checking. Programming 2018 Companion - Conference Companion of the 2nd International Conference on Art, Science, and Engineering of Programming. editor / Jennifer B. Sartor ; Stefan Marr. 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.",

keywords = "Energy consumption analysis, Model checking",

author = "Gastel, {Pascal van} and Gastel, {Bernard van} and Eekelen, {Marko C. J. D. van}",

year = "2018",

month = apr,

day = "9",

doi = "10.1145/3191697.3213805",

language = "English",

isbn = "9781450355131",

series = "ACM International Conference Proceeding Series",

publisher = "acm",

pages = "93--98",

editor = "Sartor, {Jennifer B.} and Stefan Marr",

booktitle = "Programming 2018 Companion - Conference Companion of the 2nd International Conference on Art, Science, and Engineering of Programming",

note = "Programming 2018 Companion : Conference Companion of the 2nd International Conference on Art, Science, and Engineering of Programming ; Conference date: 09-04-2018 Through 12-04-2018",

url = "https://2018.programmingconference.org/home",

}

Gastel, PV, Gastel, BV & Eekelen, MCJDV 2018, Detecting energy bugs and hotspots in control software using model checking. in JB Sartor & S Marr (eds), Programming 2018 Companion - Conference Companion of the 2nd International Conference on Art, Science, and Engineering of Programming. acm, New York, NY, ACM International Conference Proceeding Series, 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 2018 Companion - Conference Companion of the 2nd International Conference on Art, Science, and Engineering of Programming. ed. / Jennifer B. Sartor; Stefan Marr. New York, NY: acm, 2018. p. 93-98 (ACM International Conference Proceeding Series).

Research output: Chapter in Book/Report/Conference proceeding › Conference Article in proceeding › Academic › peer-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/4/9

Y1 - 2018/4/9

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.

KW - Energy consumption analysis

KW - Model checking

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 2018 Companion - Conference Companion of the 2nd International Conference on Art, Science, and Engineering of Programming

A2 - Sartor, Jennifer B.

A2 - Marr, Stefan

PB - acm

CY - New York, NY

T2 - Programming 2018 Companion

Y2 - 9 April 2018 through 12 April 2018

ER -

Gastel PV, Gastel BV, Eekelen MCJDV. Detecting energy bugs and hotspots in control software using model checking. In Sartor JB, Marr S, editors, Programming 2018 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). doi: 10.1145/3191697.3213805

Detecting energy bugs and hotspots in control software using model checking

Abstract

Publication series

Conference

Keywords

Access to Document

Fingerprint

Cite this