A model-based approach for formal verification and performance evaluation of energy harvesting architectures in IoT systems: A case study of a long-term healthcare application

Energy harvesting plays a significant role in the Internet of Things (IoT). Indeed, although numerous approaches exist to limit the system's power consumption, the energy provided by the battery remains constrained, thereby limiting the system's lifetime. Energy harvesting represents an interesting technique that allows a set of devices in an IoT architecture to operate for a potentially infinite time without the need for battery replacement or recharge. This work presents a formal modeling framework for the performance evaluation of energy harvesting architectures and strategies in IoT systems. We present a model-based approach using UPPAAL to model and analyze IoT device lifetimes and capture the energy-related behavior of nodes and various energy harvesters. Furthermore, the model is calibrated using measurements acquired from real-life IoT applications to demonstrate the effectiveness of the proposed model and its ability to investigate various energy-related aspects.