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

    Research output: Book/ReportReportProfessional

    54 Downloads (Pure)

    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
    Publication statusPublished - 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

    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; TR-CTIT-16-03).
    @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{\"e}lle Ida Antoinette} and {van de Pol}, {Jan Cornelis}",
    note = "Technical Report accompanying ACSD 2016 paper.",
    year = "2016",
    month = "4",
    day = "15",
    language = "Undefined",
    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: Book/ReportReportProfessional

    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)

    CY - Enschede

    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).