Using Real-Time Maude to Model Check Energy Consumption Behavior

Energy consumption is one of the primary non-functional concerns, especially for application programs running on systems that have limited battery capacity. A model-based analysis of energy consumption is introduced at early stages of development. As rigorous formal models of this, the power consumption automaton and a variant of linear temporal logic are proposed. Detecting unexpected energy consumption is then reduced to a model checking problem, which is unfortunately undecidable in general. This paper introduces some restrictions to the logic formulas representing energy consumption properties so that an automatic analysis is possible with Real-Time Maude.