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

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.