Formal Analysis of Android Application Behavior with Real-Time Maude

Model-based analysis is a method to study energy consumption issues at early stages of development. While hardware components are direct consumers of a battery, application programs to request these components are responsible for the total consumption. Since the behavior of these multi-thread programs is concurrent and asynchronous, the analysis on the energy consumption behavior is complicated. This paper uses Real-Time Maude for analyzing energy consumption of a whole system behavior consisting of hardware components and application programs as well as the framework. Example scenarios on detecting energy bugs demonstrate that the time-bounded analysis method using Real-Time Maude is effective.