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

    Research output: Book/ReportReportProfessional

    72 Downloads (Pure)


    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)
    ISSN (Print)1381-3625


    • METIS-316903
    • 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