Estimating Energy Wastage in Embedded Systems Using Model Checking of Timed Automata

Inefficient utilization of peripheral modules such as LTE, WiFi, and GPS in battery-operated embedded systems may cause energy wastage. We present a model-checking approach to estimate the duration that the embedded software makes such a situation in a peripheral module. We use Timed Automaton (TA) to model the embedded system, where the TA of the software part is constructed based on its control flow graph (CFG); states are defined based on the instructions that use the peripheral modules in the basic blocks, while transitions are defined based on possible flows among the states within the CFG. We abstract away other instructions within the blocks by considering the attributes of worst-case and best-case execution times in guards governing the transitions among the states. We explain how we can estimate the time duration in which the peripheral module wastes energy between two specific instructions by model checking the generated models. Regarding the evaluations on an example benchmark system, our approach found an energy wastage of 32.8%.