Model checking and evaluating QoS of batteries in MPSoC dataflow applications via hybrid automata

Waheed Ahmad; Marijn Jongerden; Mariëlle Stoelinga; Jaco van de Pol

doi:10.1109/ACSD.2016.18

Model checking and evaluating QoS of batteries in MPSoC dataflow applications via hybrid automata

Waheed Ahmad, Marijn Jongerden, Mariëlle Stoelinga, Jaco van de Pol

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

8 Citations (Scopus)

262 Downloads (Pure)

Abstract

System lifetime is a major design constraint for battery-powered mobile embedded systems. The increasing gap between the energy demand of portable devices and their battery capacities is further limiting durability of mobile devices. Thus, the guarantees over Quality of Service (QoS) of battery-constrained devices under strict battery capacities are of primary interest for mobile embedded systems’ manufacturers and stakeholders. This paper presents a novel approach for deriving QoS of applications modelled as synchronous dataflow (SDF) graphs. We map these applications on heterogeneous multiprocessor platforms that are partitioned into Voltage and Frequency Islands, together with multiple kinetic battery models (KiBaMs). By modelling the whole system as hybrid automata, and applying model-checking, we evaluate, (1) system lifetime; and (2) minimum required initial battery capacities to achieve the desired application performance. We demonstrate that our approach shows a significant improvement in terms of scalability, as compared to a priced timed automata based KiBaM model. This approach also allows early detection of design errors via model checking.

Original language	English
Title of host publication	2016 16th International Conference on Application of Concurrency to System Design (ACSD)
Place of Publication	Piscataway, NJ
Publisher	IEEE
Pages	114-123
Number of pages	10
ISBN (Electronic)	978-1-5090-2589-3
ISBN (Print)	978-1-5090-0763-9
DOIs	https://doi.org/10.1109/ACSD.2016.18
Publication status	Published - 24 Jun 2016
Event	16th International Conference on Application of Concurrency to System Design, ACSD 2016 - Toruń, Poland Duration: 19 Jun 2016 → 24 Jun 2016 Conference number: 16

Publication series

Name	Proceedings International Conference on Application of Concurrency to System Design (ACSD)
Publisher	IEEE Computer Society
Number	16
Volume	2016
ISSN (Print)	1550-4808

Conference

Conference	16th International Conference on Application of Concurrency to System Design, ACSD 2016
Abbreviated title	ACSD
Country/Territory	Poland
City	Toruń
Period	19/06/16 → 24/06/16

Keywords

Voltage and frequency scaling
Priced timed automata
EC Grant Agreement nr.: FP7/2007-2013
EC Grant Agreement nr.: FP7/318490
Battery
MPEG-4 decoder
Hybrid automata
Model checking
Data flow
Monte Carlo simulation
Heterogeneous
UPPAAL SMC
Quality of Service (QoS)
KiBaM
Kinetic battery model
Statistical model checking

Access to Document

10.1109/ACSD.2016.18

ArticleAccepted author version, 971 KB

8 Citations
1 Report

Model checking and evaluating QoS of batteries in MPSoC dataflow applications via hybrid automata (extended version)
Ahmad, W., Jongerden, M., Stoelinga, M. & van de Pol, J., 15 Apr 2016, Enschede: Centre for Telematics and Information Technology (CTIT). 33 p. (CTIT Technical Report Series; no. TR-CTIT-16-03)
Research output: Book/Report › Report › Professional

Open Access
File

Cite this

Ahmad, W., Jongerden, M., Stoelinga, M., & van de Pol, J. (2016). Model checking and evaluating QoS of batteries in MPSoC dataflow applications via hybrid automata. In 2016 16th International Conference on Application of Concurrency to System Design (ACSD) (pp. 114-123). (Proceedings International Conference on Application of Concurrency to System Design (ACSD); Vol. 2016, No. 16). IEEE. https://doi.org/10.1109/ACSD.2016.18

Ahmad, Waheed ; Jongerden, Marijn ; Stoelinga, Mariëlle et al. / Model checking and evaluating QoS of batteries in MPSoC dataflow applications via hybrid automata. 2016 16th International Conference on Application of Concurrency to System Design (ACSD). Piscataway, NJ : IEEE, 2016. pp. 114-123 (Proceedings International Conference on Application of Concurrency to System Design (ACSD); 16).

@inproceedings{21f28d7befd9486e9e40ba7da415a17e,

title = "Model checking and evaluating QoS of batteries in MPSoC dataflow applications via hybrid automata",

abstract = "System lifetime is a major design constraint for battery-powered mobile embedded systems. The increasing gap between the energy demand of portable devices and their battery capacities is further limiting durability of mobile devices. Thus, the guarantees over Quality of Service (QoS) of battery-constrained devices under strict battery capacities are of primary interest for mobile embedded systems{\textquoteright} manufacturers and stakeholders. This paper presents a novel approach for deriving QoS of applications modelled as synchronous dataflow (SDF) graphs. We map these applications on heterogeneous multiprocessor platforms that are partitioned into Voltage and Frequency Islands, together with multiple kinetic battery models (KiBaMs). By modelling the whole system as hybrid automata, and applying model-checking, we evaluate, (1) system lifetime; and (2) minimum required initial battery capacities to achieve the desired application performance. We demonstrate that our approach shows a significant improvement in terms of scalability, as compared to a priced timed automata based KiBaM model. This approach also allows early detection of design errors via model checking.",

keywords = "Voltage and frequency scaling, Priced timed automata, EC Grant Agreement nr.: FP7/2007-2013, EC Grant Agreement nr.: FP7/318490, Battery, MPEG-4 decoder, Hybrid automata, Model checking, Data flow, Monte Carlo simulation, Heterogeneous, UPPAAL SMC, Quality of Service (QoS), KiBaM, Kinetic battery model, Statistical model checking",

author = "Waheed Ahmad and Marijn Jongerden and Mari{\"e}lle Stoelinga and \{van de Pol\}, Jaco",

year = "2016",

month = jun,

day = "24",

doi = "10.1109/ACSD.2016.18",

language = "English",

isbn = "978-1-5090-0763-9",

series = "Proceedings International Conference on Application of Concurrency to System Design (ACSD)",

publisher = "IEEE",

number = "16",

pages = "114--123",

booktitle = "2016 16th International Conference on Application of Concurrency to System Design (ACSD)",

address = "United States",

note = "16th International Conference on Application of Concurrency to System Design, ACSD 2016, ACSD ; Conference date: 19-06-2016 Through 24-06-2016",

}

Ahmad, W, Jongerden, M, Stoelinga, M & van de Pol, J 2016, Model checking and evaluating QoS of batteries in MPSoC dataflow applications via hybrid automata. in 2016 16th International Conference on Application of Concurrency to System Design (ACSD). Proceedings International Conference on Application of Concurrency to System Design (ACSD), no. 16, vol. 2016, IEEE, Piscataway, NJ, pp. 114-123, 16th International Conference on Application of Concurrency to System Design, ACSD 2016, Toruń, Poland, 19/06/16. https://doi.org/10.1109/ACSD.2016.18

Model checking and evaluating QoS of batteries in MPSoC dataflow applications via hybrid automata. / Ahmad, Waheed; Jongerden, Marijn; Stoelinga, Mariëlle et al.
2016 16th International Conference on Application of Concurrency to System Design (ACSD). Piscataway, NJ: IEEE, 2016. p. 114-123 (Proceedings International Conference on Application of Concurrency to System Design (ACSD); Vol. 2016, No. 16).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Model checking and evaluating QoS of batteries in MPSoC dataflow applications via hybrid automata

AU - Ahmad, Waheed

AU - Jongerden, Marijn

AU - Stoelinga, Mariëlle

AU - van de Pol, Jaco

N1 - Conference code: 16

PY - 2016/6/24

Y1 - 2016/6/24

N2 - System lifetime is a major design constraint for battery-powered mobile embedded systems. The increasing gap between the energy demand of portable devices and their battery capacities is further limiting durability of mobile devices. Thus, the guarantees over Quality of Service (QoS) of battery-constrained devices under strict battery capacities are of primary interest for mobile embedded systems’ manufacturers and stakeholders. This paper presents a novel approach for deriving QoS of applications modelled as synchronous dataflow (SDF) graphs. We map these applications on heterogeneous multiprocessor platforms that are partitioned into Voltage and Frequency Islands, together with multiple kinetic battery models (KiBaMs). By modelling the whole system as hybrid automata, and applying model-checking, we evaluate, (1) system lifetime; and (2) minimum required initial battery capacities to achieve the desired application performance. We demonstrate that our approach shows a significant improvement in terms of scalability, as compared to a priced timed automata based KiBaM model. This approach also allows early detection of design errors via model checking.

AB - System lifetime is a major design constraint for battery-powered mobile embedded systems. The increasing gap between the energy demand of portable devices and their battery capacities is further limiting durability of mobile devices. Thus, the guarantees over Quality of Service (QoS) of battery-constrained devices under strict battery capacities are of primary interest for mobile embedded systems’ manufacturers and stakeholders. This paper presents a novel approach for deriving QoS of applications modelled as synchronous dataflow (SDF) graphs. We map these applications on heterogeneous multiprocessor platforms that are partitioned into Voltage and Frequency Islands, together with multiple kinetic battery models (KiBaMs). By modelling the whole system as hybrid automata, and applying model-checking, we evaluate, (1) system lifetime; and (2) minimum required initial battery capacities to achieve the desired application performance. We demonstrate that our approach shows a significant improvement in terms of scalability, as compared to a priced timed automata based KiBaM model. This approach also allows early detection of design errors via model checking.

KW - Voltage and frequency scaling

KW - Priced timed automata

KW - EC Grant Agreement nr.: FP7/2007-2013

KW - EC Grant Agreement nr.: FP7/318490

KW - Battery

KW - MPEG-4 decoder

KW - Hybrid automata

KW - Model checking

KW - Data flow

KW - Monte Carlo simulation

KW - Heterogeneous

KW - UPPAAL SMC

KW - Quality of Service (QoS)

KW - KiBaM

KW - Kinetic battery model

KW - Statistical model checking

U2 - 10.1109/ACSD.2016.18

DO - 10.1109/ACSD.2016.18

M3 - Conference contribution

SN - 978-1-5090-0763-9

T3 - Proceedings International Conference on Application of Concurrency to System Design (ACSD)

SP - 114

EP - 123

BT - 2016 16th International Conference on Application of Concurrency to System Design (ACSD)

PB - IEEE

CY - Piscataway, NJ

T2 - 16th International Conference on Application of Concurrency to System Design, ACSD 2016

Y2 - 19 June 2016 through 24 June 2016

ER -

Ahmad W, Jongerden M, Stoelinga M , van de Pol J. Model checking and evaluating QoS of batteries in MPSoC dataflow applications via hybrid automata. In 2016 16th International Conference on Application of Concurrency to System Design (ACSD). Piscataway, NJ: IEEE. 2016. p. 114-123. (Proceedings International Conference on Application of Concurrency to System Design (ACSD); 16). doi: 10.1109/ACSD.2016.18

Model checking and evaluating QoS of batteries in MPSoC dataflow applications via hybrid automata

Abstract

Publication series

Conference

Keywords

Access to Document

Fingerprint

Research output

Model checking and evaluating QoS of batteries in MPSoC dataflow applications via hybrid automata (extended version)

Cite this