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