Analyzing Energy Leaks of Android Applications Using Event-B.

The number of mobile applications downloaded recently from Google stores increase steadily. It is believed that mobile applications market revenues will grow fast and receive more attention from software developers. Even though, hardware technologies and operating systems have made a big contribution to improve the battery capacity, power consumption is one of the most important and crucial non-functional properties of mobile applications. Many approaches have been dedicated for analyzing and optimizing the power consumption at different levels. This paper proposes a method for analyzing energy leaks of Android application at the design phase. First, it introduces a formalization of an event-based power consumption model. After that, the paper presents a method to translate this model to Event-B notations. Based on the target model, it is able to check if the application leads to energy leaks or violates the power consumption constraints based on formal proofs. Finally, the motivating examples are shown for the illustration purpose. [ABSTRACT FROM AUTHOR]