A Model-Checking Static Analysis of Task-Based Energy Neutrality for Energy Harvesting IoT

We address the problem of energy neutrality in energy harvesting IoT devices by means of a model checking approach, aiming at analyzing the dynamics of the battery charge in energy-neutral IoT devices. Our approach allows to compute the best task schedule and to study the maximum utility when operating on other parameters such as the initial battery charge, the number and structure of the available tasks, the size of the photo-voltaic panel that recharges the device, the day of the year, and the variable weather conditions that affect the energy production. The simulations confirm the state space explosion typical of model checking, but also hint that a small number of alternative tasks can achieve an overall utility very close to a large number of tasks. This conjecture has a strong practical relevance since it can pave the way to the wider adoption of energy neutrality concept in low-power IoT devices.