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

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    5 Citations (Scopus)
    59 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 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
    Publication statusPublished - 24 Jun 2016
    Event16th International Conference on Application of Concurrency to System Design, ACSD 2016 - Toruń, Poland
    Duration: 19 Jun 201624 Jun 2016
    Conference number: 16

    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

    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. https://doi.org/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. pp. 114-123
    @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’ 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{\"e}lle Ida Antoinette} and {van de Pol}, {Jan Cornelis}",
    note = "eemcs-eprint-27106",
    year = "2016",
    month = "6",
    day = "24",
    doi = "10.1109/ACSD.2016.18",
    language = "Undefined",
    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/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, 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: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    TY - GEN

    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

    CY - USA

    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 https://doi.org/10.1109/ACSD.2016.18