Abstract

System lifetime is always a major design impediment for battery-powered mobile embedded systems such as, cell phones and satellites. The increasing gap between energy demand of portable devices and their battery capacities is further limiting durability of mobile devices. For example, energy-hungry applications like video streaming pose serious limitations on the system lifetime. Thus, guarantees over Quality of Service (QoS) of battery constrained devices under strict battery capacities is a primary interest for mobile embedded systems' manufacturers and other stakeholders. This paper presents a novel approach for deriving QoS, for applications modelled as synchronous dataflow (SDF) graphs. These applications are mapped on heterogeneous multiprocessor platforms that are partitioned into Voltage and Frequency Islands, together with multiple kinetic battery models (KiBaMs). By modelling whole system as hybrid automata, and applying model-checking, we evaluate QoS in terms of, (1) achievable application performance within the given batteries' capacities; and (2) minimum required batteries' capacities to achieve desired application performance. We demonstrate that our approach shows a signicant improvement in terms of scalability, as compared to priced timed automata based KiBaM model. This approach also allows early detection of design errors via model checking.
Original languageUndefined
Place of PublicationEnschede
PublisherCentre for Telematics and Information Technology (CTIT)
Number of pages33
StatePublished - 15 Apr 2016

Publication series

NameCTIT Technical Report Series
PublisherUniversity of Twente, Centre for Telematics and Information Technology (CTIT)
No.TR-CTIT-16-03
ISSN (Print)1381-3625

Fingerprint

Quality of service
Model checking
Embedded systems
Video streaming
Mobile devices
Scalability
Durability
Energy gap
Kinetics

Keywords

  • METIS-316903
  • UPPAAL SMC
  • EWI-26966
  • EC Grant Agreement nr.: FP7/2007-2013
  • EC Grant Agreement nr.: FP7/318490
  • battery lifetime
  • battery capacity
  • voltage-frequency island
  • Throughput
  • IR-100294
  • Batteries
  • Hybrid Automata
  • Model Checking
  • MPEG-4
  • Data flow
  • SDF
  • Heterogeneous
  • Quality of Service
  • UPPAAL
  • QoS
  • Video Frames
  • Kinetic Battery Model
  • Statistical Model Checking
  • Timed Automata
  • Priced Timed Automata

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 (extended version). (CTIT Technical Report Series; No. TR-CTIT-16-03). Enschede: Centre for Telematics and Information Technology (CTIT).

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 (extended version).

Enschede : Centre for Telematics and Information Technology (CTIT), 2016. 33 p. (CTIT Technical Report Series; No. TR-CTIT-16-03).

Research output: ProfessionalReport

@book{68bb351bed5a411ba77ad209270b00cd,
title = "Model checking and evaluating QoS of batteries in MPSoC dataflow applications via hybrid automata (extended version)",
abstract = "System lifetime is always a major design impediment for battery-powered mobile embedded systems such as, cell phones and satellites. The increasing gap between energy demand of portable devices and their battery capacities is further limiting durability of mobile devices. For example, energy-hungry applications like video streaming pose serious limitations on the system lifetime. Thus, guarantees over Quality of Service (QoS) of battery constrained devices under strict battery capacities is a primary interest for mobile embedded systems' manufacturers and other stakeholders. This paper presents a novel approach for deriving QoS, for applications modelled as synchronous dataflow (SDF) graphs. These applications are mapped on heterogeneous multiprocessor platforms that are partitioned into Voltage and Frequency Islands, together with multiple kinetic battery models (KiBaMs). By modelling whole system as hybrid automata, and applying model-checking, we evaluate QoS in terms of, (1) achievable application performance within the given batteries' capacities; and (2) minimum required batteries' capacities to achieve desired application performance. We demonstrate that our approach shows a signicant improvement in terms of scalability, as compared to priced timed automata based KiBaM model. This approach also allows early detection of design errors via model checking.",
keywords = "METIS-316903, UPPAAL SMC, EWI-26966, EC Grant Agreement nr.: FP7/2007-2013, EC Grant Agreement nr.: FP7/318490, battery lifetime, battery capacity, voltage-frequency island, Throughput, IR-100294, Batteries, Hybrid Automata, Model Checking, MPEG-4, Data flow, SDF, Heterogeneous, Quality of Service, UPPAAL, QoS, Video Frames, Kinetic Battery Model, Statistical Model Checking, Timed Automata, Priced Timed Automata",
author = "W. Ahmad and M.R. Jongerden and Stoelinga, {Mariëlle Ida Antoinette} and {van de Pol}, {Jan Cornelis}",
note = "Technical Report accompanying ACSD 2016 paper.",
year = "2016",
month = "4",
series = "CTIT Technical Report Series",
publisher = "Centre for Telematics and Information Technology (CTIT)",
number = "TR-CTIT-16-03",
address = "Netherlands",

}

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 (extended version). CTIT Technical Report Series, no. TR-CTIT-16-03, Centre for Telematics and Information Technology (CTIT), Enschede.

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

Enschede : Centre for Telematics and Information Technology (CTIT), 2016. 33 p. (CTIT Technical Report Series; No. TR-CTIT-16-03).

Research output: ProfessionalReport

TY - BOOK

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

AU - Ahmad,W.

AU - Jongerden,M.R.

AU - Stoelinga,Mariëlle Ida Antoinette

AU - van de Pol,Jan Cornelis

N1 - Technical Report accompanying ACSD 2016 paper.

PY - 2016/4/15

Y1 - 2016/4/15

N2 - System lifetime is always a major design impediment for battery-powered mobile embedded systems such as, cell phones and satellites. The increasing gap between energy demand of portable devices and their battery capacities is further limiting durability of mobile devices. For example, energy-hungry applications like video streaming pose serious limitations on the system lifetime. Thus, guarantees over Quality of Service (QoS) of battery constrained devices under strict battery capacities is a primary interest for mobile embedded systems' manufacturers and other stakeholders. This paper presents a novel approach for deriving QoS, for applications modelled as synchronous dataflow (SDF) graphs. These applications are mapped on heterogeneous multiprocessor platforms that are partitioned into Voltage and Frequency Islands, together with multiple kinetic battery models (KiBaMs). By modelling whole system as hybrid automata, and applying model-checking, we evaluate QoS in terms of, (1) achievable application performance within the given batteries' capacities; and (2) minimum required batteries' capacities to achieve desired application performance. We demonstrate that our approach shows a signicant improvement in terms of scalability, as compared to priced timed automata based KiBaM model. This approach also allows early detection of design errors via model checking.

AB - System lifetime is always a major design impediment for battery-powered mobile embedded systems such as, cell phones and satellites. The increasing gap between energy demand of portable devices and their battery capacities is further limiting durability of mobile devices. For example, energy-hungry applications like video streaming pose serious limitations on the system lifetime. Thus, guarantees over Quality of Service (QoS) of battery constrained devices under strict battery capacities is a primary interest for mobile embedded systems' manufacturers and other stakeholders. This paper presents a novel approach for deriving QoS, for applications modelled as synchronous dataflow (SDF) graphs. These applications are mapped on heterogeneous multiprocessor platforms that are partitioned into Voltage and Frequency Islands, together with multiple kinetic battery models (KiBaMs). By modelling whole system as hybrid automata, and applying model-checking, we evaluate QoS in terms of, (1) achievable application performance within the given batteries' capacities; and (2) minimum required batteries' capacities to achieve desired application performance. We demonstrate that our approach shows a signicant improvement in terms of scalability, as compared to priced timed automata based KiBaM model. This approach also allows early detection of design errors via model checking.

KW - METIS-316903

KW - UPPAAL SMC

KW - EWI-26966

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

KW - EC Grant Agreement nr.: FP7/318490

KW - battery lifetime

KW - battery capacity

KW - voltage-frequency island

KW - Throughput

KW - IR-100294

KW - Batteries

KW - Hybrid Automata

KW - Model Checking

KW - MPEG-4

KW - Data flow

KW - SDF

KW - Heterogeneous

KW - Quality of Service

KW - UPPAAL

KW - QoS

KW - Video Frames

KW - Kinetic Battery Model

KW - Statistical Model Checking

KW - Timed Automata

KW - Priced Timed Automata

M3 - Report

T3 - CTIT Technical Report Series

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

PB - Centre for Telematics and Information Technology (CTIT)

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 (extended version). Enschede: Centre for Telematics and Information Technology (CTIT), 2016. 33 p. (CTIT Technical Report Series; TR-CTIT-16-03).