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 languageUndefined
Title of host publicationProceedings of the 16th International Conference on Application of Concurrency to System Design, ACSD 2016
Place of PublicationUSA
PublisherIEEE Computer Society
Pages114-123
Number of pages10
ISBN (Print)1550-4808
DOIs
StatePublished - 24 Jun 2016
Event16th International Conference on Application of Concurrency to System Design, ACSD 2016 - Toruń, Poland

Publication series

Name
PublisherIEEE Computer Society
ISSN (Print)1550-4808

Conference

Conference16th International Conference on Application of Concurrency to System Design, ACSD 2016
Abbreviated titleACSD
CountryPoland
CityToruń
Period19/06/1624/06/16

Fingerprint

Embedded systems
Quality of service
Mobile devices
Scalability
Durability
Kinetics

Keywords

  • Voltage and Frequency Scaling
  • METIS-318473
  • Priced Timed Automata
  • EWI-27106
  • EC Grant Agreement nr.: FP7/2007-2013
  • EC Grant Agreement nr.: FP7/318490
  • IR-100968
  • 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

Cite this

Ahmad, W., Jongerden, M. R., Stoelinga, M. I. A., & van de Pol, J. C. (2016). Model checking and evaluating QoS of batteries in MPSoC dataflow applications via hybrid automata. In Proceedings of the 16th International Conference on Application of Concurrency to System Design, ACSD 2016 (pp. 114-123). USA: IEEE Computer Society. DOI: 10.1109/ACSD.2016.18

Ahmad, W.; Jongerden, M.R.; Stoelinga, Mariëlle Ida Antoinette; van de Pol, Jan Cornelis / Model checking and evaluating QoS of batteries in MPSoC dataflow applications via hybrid automata.

Proceedings of the 16th International Conference on Application of Concurrency to System Design, ACSD 2016. USA : IEEE Computer Society, 2016. p. 114-123.

Research output: Scientific - peer-reviewConference contribution

@inbook{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’ 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, METIS-318473, Priced Timed Automata, EWI-27106, EC Grant Agreement nr.: FP7/2007-2013, EC Grant Agreement nr.: FP7/318490, IR-100968, 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 = "W. Ahmad and M.R. Jongerden and Stoelinga, {Mariëlle Ida Antoinette} and {van de Pol}, {Jan Cornelis}",
note = "eemcs-eprint-27106",
year = "2016",
month = "6",
doi = "10.1109/ACSD.2016.18",
isbn = "1550-4808",
publisher = "IEEE Computer Society",
pages = "114--123",
booktitle = "Proceedings of the 16th International Conference on Application of Concurrency to System Design, ACSD 2016",
address = "United States",

}

Ahmad, W, Jongerden, MR, Stoelinga, MIA & van de Pol, JC 2016, Model checking and evaluating QoS of batteries in MPSoC dataflow applications via hybrid automata. in Proceedings of the 16th International Conference on Application of Concurrency to System Design, ACSD 2016. IEEE Computer Society, USA, pp. 114-123, 16th International Conference on Application of Concurrency to System Design, ACSD 2016, Toruń, Poland, 19-24 June. DOI: 10.1109/ACSD.2016.18

Model checking and evaluating QoS of batteries in MPSoC dataflow applications via hybrid automata. / Ahmad, W.; Jongerden, M.R.; Stoelinga, Mariëlle Ida Antoinette; van de Pol, Jan Cornelis.

Proceedings of the 16th International Conference on Application of Concurrency to System Design, ACSD 2016. USA : IEEE Computer Society, 2016. p. 114-123.

Research output: Scientific - peer-reviewConference contribution

TY - CHAP

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

AU - Ahmad,W.

AU - Jongerden,M.R.

AU - Stoelinga,Mariëlle Ida Antoinette

AU - van de Pol,Jan Cornelis

N1 - eemcs-eprint-27106

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 - METIS-318473

KW - Priced Timed Automata

KW - EWI-27106

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

KW - EC Grant Agreement nr.: FP7/318490

KW - IR-100968

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

KW - 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 - 1550-4808

SP - 114

EP - 123

BT - Proceedings of the 16th International Conference on Application of Concurrency to System Design, ACSD 2016

PB - IEEE Computer Society

ER -

Ahmad W, Jongerden MR, Stoelinga MIA, van de Pol JC. Model checking and evaluating QoS of batteries in MPSoC dataflow applications via hybrid automata. In Proceedings of the 16th International Conference on Application of Concurrency to System Design, ACSD 2016. USA: IEEE Computer Society. 2016. p. 114-123. Available from, DOI: 10.1109/ACSD.2016.18