=Paper= {{Paper |id=Vol-1084/paper5 |storemode=property |title=Model-based Power Consumption Analysis of Smartphone Applications |pdfUrl=https://ceur-ws.org/Vol-1084/paper5.pdf |volume=Vol-1084 |dblpUrl=https://dblp.org/rec/conf/models/Nakajima13 }} ==Model-based Power Consumption Analysis of Smartphone Applications== https://ceur-ws.org/Vol-1084/paper5.pdf

Model-based Power Consumption Analysis of
Smartphone Applications

Shin NAKAJIMA

National Institute of Informatics⋆⋆
Tokyo, Japan
nkjm@nii.ac.jp

Abstract. Unexpected power consumption of smartphone applications
is a nuisance because the battery capacity is limited. Such energy bugs
(ebugs) are currently detected only at runtime. Some ebugs, however,
are desirable to detect at the early stage of the development because
they are design faults. This paper proposes a formal model, the power
consumption automaton, to account for the power consumption, and
discusses how the tool-assisted analysis is conducted.

Keywords: Android, Energy Bugs, Stopwatch Automaton, UPPAAL,
Realtime Maude, Sampling Abstraction

1 Introduction

Smartphones are compact and small, but are a complex system to consist of
many components. All of them have impact on the power consumption of the
battery, but their causal relationships are not clear owing to the complexity of
the multi-layered architecture [1]. A functionally correct application may suﬀer
from unexpected power consumption, which is called energy bugs (ebugs) [14].
Detecting such ebugs currently uses energy proﬁlers (cf. [15]), which monitor the
program execution at runtime to see whether power drains exist.
Smartphones adapt an aggressive power saving strategy to reduce the battery
power consumption. Some applications, however, keep the smartphone awake
even during the inactivity periods. To meet this demand, the Android framework
provides application interfaces (API) for the power management [1]. The API
is a two-edged sword; it is usable while it may introduce further ebugs due to
improper uses of the API. These ebugs are desirable to detect at the early stage
of the development because they are design faults.
This paper proposes a new model-based approach to the representation and
analysis of the asynchronous power consumption of Android applications. We
introduce a formal model, the power consumption automaton (PCA), show how
the PCA is analyzed with existing tools and present some discussions based on
our experience.
⋆⋆
Also aﬃliated with The Graduate University for Advanced Studies (SOKENDAI)
App Service

Android Framework / Linux

LCD CPU (DVFS) Network Peripheral

Ba!ery

Fig. 1. Conﬁguration

2 Power Consumption in Android
2.1 Power Management
Figure 1 shows the conﬁguration of Android smartphones focused on the power
consumption. The Android framework together with the Linux kernel provides
basic features to the application programs, app and service. Android app is an
application process to provide GUI to the user, while Android service does not
use GUI and is a backgound process. All of them may be multi-threaded to have
concurrency. In addition, the application processes use the hardware components
such as networks or peripherals. These, except for the docking station, are the
consumers of the battery power.
The Android framework encapsulates the underlying components for pro-
gramming tasks easy. It, however, makes it hard to know the power consumption
behavior precisely. The framework adapts an aggressive power saving strategy;
the power control subsystem automatically forces the system to sleep when the
user does not touch the screen for some periods of time.
Some app may prohibit the power saving, and the Android framework pro-
vides the wake locks for the power management. An app can request CPU re-
sources with wake locks (WakeLock), and CPU is kept awake while some active
locks remain. An acquired wake lock should have a matching release call. Other-
wise, the wake lock is kept alive even after the caller program is destroyed. Such
improper uses of wake locks result in ebugs. These ebugs can, in principle, be
eliminated at the early stage of the development because they are design faults.

2.2 Wi-Fi Subsystem
This paper uses the Wi-Fi component as a concrete example to discuss the
motivation and technical details of the proposal. Figure 2 is an example measured
energy proﬁle of a Wi-Fi client in Nexus One operating in the power save mode
(PSM) [3]. It is taken from [11] to be modiﬁed a little for illustrative purposes.
The Wi-Fi client, or station (STA), is in the passive scan mode. The access
point (AP) periodically sends beacon signals to notify the STA to start trans-
ferring data. Figure 2 shows that the STA is ﬁrst in the Deep Sleep state, and
Power
(mW)
High Power

500

Beacon Idle Listen Inac!vity !mer

Deep Deep
Sleep Light Sleep Sleep

0
0.0 1.0 2.0 3.0 Time (s)

Fig. 2. Wi-Fi Energy Proﬁle (Adapted from [11])

then goes to the High Power state to exchange various frames. The STA stays in
the Idle Listen state to see if there are further frames to come. The STA moves
down to the Light Sleep state when it recognizes a no-more-data ﬂag in the
data frame. The STA stays in this state for a while to be ready for further data
transfer occurring soon. The STA returns to the Deep Sleep state by a time-out
event of the inactivity timer.
The Wi-Fi subsystem also adapts the notion of wake locks for the power
management. WifiManager provides a method to control over WifiLock [1]. It
allows an application to keep the Wi-Fi radio awake. The STA, while a lock is
active, stays in the Light Sleep, but does not go to the Deep Sleep state .

2.3 Power Consumption Model
If the graph in Figure 2 is represented as a function F (t), the total power con-
sumption (P (T )) from 0 to a time T is obtained by the accumulation, or integral
∫T
of F (t); P (T ) = 0 F (t)dt. As the above explanation with Figure 2 suggests,
the states of the STA are changed in either event-trigger (signal or frame) or
time-trigger (periodic or timeout) manners. Such changes can be represented
by state-transition system consisting of power states. Figure 3 is an example
state-transition system of Wi-Fi STA operating in PSM.
This paper focuses on the analysis of unexpected power consumption, but
does not try to predict the power consumption behavior in a numerically precise
manner. It is suﬃce to check whether the whole system stays at some particular
power state in a unexpectedly long time. F (t) can be approximated by a linear
PS
funtion of time. Let P (tS , tE ) be the consumed power in the state P S from tS
PS
to tE that P (tS , tE ) =C ×(tE − tS ) with a constant C P S . P (T ) becomes a
PS

sum of the power consumptions in all the states that the STA transition system
visits.
∑
N −1
PS
P (T ) = P (ti , ti+1 )
i=0

PS PS
where t0 = 0 and tN = T . P (tS , tE ) can be written as P (t) , equal to
DeepSleep
C P S ×t, with t = tE − tS . For example, P (t) refers to the sum of the
Data transfer
[not more]
High Power / reset inac!vity !mer

beacon Beacon Data transfer
[TIM] [TIM] [more]

Authen!ca!on Idle Listen

beacon Associa!on
beacon
[not TIM] [TIM]
beacon
[not TIM]
Deep Light
Sleep Sleep beacon
[not TIM]
expire inac!vity !mer

Fig. 3. Behavioral Model of STA

power consumed as the drain currents of the radio circuits and that needed to
process the beacon signals (see Figure 2). A state, DeepSleep for example, is
visited many times while the Wi-Fi subsystem is enabled.

3 Model-Based Analysis of Power Consumption

3.1 Power Consumption Automaton

We introduce a state transition system, power consumption automaton1 , to be a
formal representation. Power consumption automaton (PCA) is a 6-tuple, whose
deﬁnition follows the presentation in [4], ⟨ Loc, V ar, Lab, Edg, Act, Inv ⟩. The
components are explained below.

1. Loc is a ﬁnite set of locations to represent power states.
2. V ar is a ﬁnite set of real-valued variables, A valuation v for the variables is a
function to assign a real-value v(x)∈R to each variable x∈V ar. V represents
the set of valuations (v).
3. Lab is a ﬁnite set of synchronization labels to contain the stutter label τ ∈Lab.
4. Edg is a ﬁnite set of transitions. Each transition e is a tuple ⟨l, a, µ, l′ ⟩ where
l, l′ ∈Loc are a source and a target, a∈Lab is a synchronization label, and µ
is an action deﬁned by a guarded set of assignments (updates)
ψ ⇒ { x := αx | x∈V ar }.
where the guard ψ is a linear formula over the variables, and αx is a linear
term.
5. Act is a mapping from locations in Loc to a set of activities to represent the
ﬂow dynamics. Act(l) is a diﬀerential equation of the form dP/dt = K with
K∈Z. K is C l for the case of power consumption and 1 for clock such as the
inactivity timer.
6. Inv is a mapping from locations in Loc to invariants Inv(l)⊆V . Inv(l) is
deﬁned by a linear formula ϕ over V ar.
1
It was introduced ﬁrst in an oral presentation [12].
Two PCAs synchronize on the common set of labels Lab1 ∩Lab2 . Whenever
P CA1 makes a discrete transition with a synchronization label a∈(Lab1 ∩Lab2 ),
P CA2 also performs a discrete transition. Therefore, concurrency is naturally
represented; an example is found in Figure 4.
PCA is a strict subclass of linear hybrid automaton (LHA) [5]. LHA is a
hybrid automaton whose guards (ψ), updates (µ), and invariants (ϕ) are only
linear expressions, and the dynamics are speciﬁed using diﬀerential inequalities
that are linear constraints over ﬁrst-order derivatives (C1 ≤ dx/dt ≤ C2 ). The
dynamics of PCA are diﬀerential equalities of the form, dP/dt = C l for the
power consumption, and dX/dt = 1 for the clock variable X, which are linear
equality constraints over ﬁrst-order derivatives. PCA is a subclass of LHA.

3.2 Reachability Problem
The algorithmic analysis methods were studied for linear hybrid automaton
(LHA), speciﬁcally the reachability analysis over inﬁnite state spaces generated
by the labeled transition system (LTS) associated with the LHA [4].
LHA has several special cases such as a timed automaton (TA), a multirate
timed system (MTS), n-rate timed system (nRTS), and a stopwatch automaton
(SWA). An LHA is simple if the location invariants (ϕ) and transition guards
(ψ) are of the form x≤k or k≤x for x∈V ar and k∈Z. A variable x is a clock if
Act(l, x) = 1 for each location and µ(e, x)∈{0, x} for each edge. A skewed clock is
a clock to change with time at some rate k∈Z; Act(l, x) = k and µ(e, x)∈{0, x}.
A TA is a simple linear hybrid automaton with clocks. An MTS is a linear
hybrid automaton whose clocks are skewed. An nRTS is an MTS whose skewed
clocks proceed at n diﬀerent rates. A SWA is a TA where Act(l, x)∈{0, 1} and
µ(e, x)∈{0, x}. The reachability problem is known decidable for TA and simple
MTS, but undecidable for other cases even if they are simple.

3.3 Analysis of Power Consumption Automaton
We assume here a PCA with N power states, each of which consumes diﬀerent
j
electric power as P (t) = C j ×t (j = 0. . .N − 1). The property to check may take
a form of 2(P ow≤M ax), which mentions that the total power (P ow) is always
within a given M ax. We consider how PCA is encoded in some subclass of LHA
to see the decidability of the PCA reachability analysis.
First, a PCA is encoded as an N-rate timed system. A skewed clock P ow
is introduced, which changes at the rate of C j in the power state j, proceeding
at N diﬀerent rates. P ow accumulates all the consumed power. Alternatively,
j
a PCA is represented as an MTS. We regard each P (t) to be a skewed clock
j j j
X to change at a ﬁxed rate of C . Since X changes with time only when the
PCA stays on that state j, X j must be stopped in all the other states. PCA
is now a multirate stopwatch automaton,
∑N −1 where the total power consumption
is calculated such that P ow = j=0 X j . PCA is more expressive than either
MTS or SWA. Some over-approximation method is needed in the tool-assisted
analysis.
Data transfer
[(not more) and (not locked)]
High Power / reset inac!vity !mer

Init excep!on
release Beacon Data transfer
beacon
/ n:=0; [TIM] [TIM] [more]
lock := false Data transfer
Unlock [(not more)
Authen!ca!on Idle Listen
and locked]
Associa!on beacon
release [ n == 1] acquire beacon beacon [TIM]
/ n--; lock := false / n++; lock := true [not TIM] beacon [not TIM
[(not TIM) and locked]
Lock Deep and (not locked)] Light
release acquire Sleep Sleep
[n > 1] / n++ beacon
expire inac!vity !mer
/ n--; [not TIM]

Fig. 4. Wi-Fi PSM with Wake Lock

4 Analysis with Automatic Tools
This section presents two methods of representing and analyzing the PCA with
two automatic tools, UPPAAL [7][9] and Readltime Maude [2][13].

4.1 Wi-Fi Power Consumption Automaton
The Android framework provides WifiLock to allow an application to keep the
Wi-Fi awake [1]. Figure 4 shows diagrammatic representations of the PCAs for
a wake lock (the left) and a Wi-Fi STA (the right).
The reference-counted WifiLock in Figure 4 shows that the acquire() and
release() must be balanced, which is similar to counting semaphore. The
acquire() method locks the Wi-Fi on until the release() is called to turn
it oﬀ. The locked Wi-Fi stays in the Idle Listen state even when the data
transfer ends with the no-more-data ﬂag on2 .

4.2 Analysis using UPPAALL
This subsection sketches how the PCA is encoded in the stopwatch-extension of
UPPAAL [7][9].
Let XP S be a clock variable introduced for a power state P S. We add invari-
ants dXP S /dt = 0 to all the states except in the state P S. XP S must proceed
in the state P S and thus the invariant there is dXP S /dt = 1. Figure 5 shows
four clock variables, for recording how long the Wi-Fi client stays in each state.
The ﬁrst-order derivative of xIL (written xIL’), for example, is set to 0 in all
the states other than Idle Listen.
We then use a query expression of the form A2(XP S ≤AP S ) where AP S is
a constant to refer to the maximum power consumption allowed for this power
state. For example, a counter-example is generated for the case of A2(XIL ≤AIL )
when WiFi lock bugs are hidden in the design.
2
Comapre Figure 4 with Figure 3 to study the diﬀerences.
Fig. 5. Wi-Fi Client with Lock (Taken from [12])

4.3 Analysis Using Realtime Maude

PCA is encoded as an n-rate timed system, represented in Realtime Maude.

Realtime Maude Realtime Maude [2][13] is an extension of Maude [8] for the
application of rewriting logic to the executable speciﬁcations of realtime and
hybrid systems. Realtime Maude provides two kinds of rewrite rules, the instan-
taneous rules and tick rules. Let T (A) be a term. A conditional instantaneous
rule with a label r takes a form below.

r : T (A) −→ T (A′ ) if C .

The term on the left-hand side (T (A)) is rewritten to the right-hand side one
(T (A′ )), while the rule is ﬁred only when the side condition C is true.
The tick rules are responsible for time progress. Let T be a set of terms,
a snapshot of the whole system. A tick rule works on { T } nondeterministi-
cally. Time-nondeterministic systems are analyzed under sampling abstractions,
in which the maximum time elapsed (mte) plays an important role.

l : { T } −→ { δ(T, τl ) } in time τl if τl ≤ mte(T )

The rule states that the amount of time τl is passed in rewriting T to δ(T, τl ).
mte(T ) is the upper limit of the time progress, and thus it instructs the analysis
method to ﬁre transitions at some time so long as the side condition is satisﬁed.
The transition is ﬁred at least once in the time interval that mte(T ) speciﬁes.
Two functions, mte and δ, are deﬁned for each term T .
Realtime Maude supports the timed model-checking of the property ex-
pressed in linear temporal logic (LTL) under the sampling abstraction.
Encoding Wi-Fi PCA in Realtime Maude The Wi-Fi STA in Figure 4
requires a set of rewriting rules, and the below shows some fragments of its be-
havior only. First, we introduce a wif iST A term to represent the PCA to have
four components; Loc for power states, P ower for accumulated power consump-
tion, a Boolean ﬂag Bool for the WiﬁLock status, and T ime for the inactivity
timer.

op wif iST A : Loc P ower Bool T ime −→ System

Here are three instantaneous rules; transitions from the High Power state when
wif iST A receives data with ﬂags.

h1: wif iST A(HighP ower, P, B, X) Data(M ore)
−→ wif iST A(IdleListen, P, B, X)
h2: wif iST A(HighP ower, P, f alse, X) Data(N oM ore)
−→ wif iST A(LightSleep, P, f alse, X) Reset
h3: wif iST A(HighP ower, P, true, X) Data(N oM ore)
−→ wif iST A(IdleListen, P, true, X)

δ calculates the consumed power at each state. The ﬁrst equation below shows
the case for the High Power state, and the rests describe the two cases for the
Light Sleep state. They select appropriate new states depending on the status
of the inactivity timer. C stands for the timeout constant.

δ(wif iST A(HighP ower, P, B, X), τ )
= wif iST A(HighP ower, P + C HP ×τ, B, X)
δ(wif iST A(LightSleep, P, B, X), τ )
= wif iST A(LightSleep, P + C LS ×τ, B, X + τ ) if X < C − τ
δ(wif iST A(LightSleep, P, B, X), τ )
= wif iST A(DeepSleep, P + C LS ×τ, B, X + τ ) if X ≥ C − τ

The inactivity timer is time-dependent component in wif iST A. mte is deﬁned
so that the timer is checked at least once at some critical intervals.

mte(wif iST A(L, P, B, X)) = inf if not(L = LightSleep)
mte(wif iST A(L, P, B, X)) = C − X if (L = LightSleep)

4.4 Discussion
Section 3.3 presented two of PCA encoding methods with LHA subclasses; (a)
a multirate stopwatch automaton, and (b) an n-rated timed system.
The approach with the stopwatch-extension of UPPAAL has a slight restric-
tion of the case (a) above since the clocks are not skewed. Therefore, query
checking is performed separately for each clock. A sum of clock variables does
not make sense due to the symbolic model-checking algorithm. The encoding
with Realtime Maude adapts the approach (b). We introduced a single skewed
clock variable P ow to accumulate the consumed power. P ow proceeds at a dif-
ferent rate in each power state. Therefore, the total amount of the consumed
power can be analyzed, although the sampling abstraction and time-bounded
search methods have to be employed.
This paper used the Wi-Fi subsystem as the example PCA, not an Android
application, while the motivation of this work was removing ebugs from the
applications at the design stage. Since an application uses a wide variety of
components, all the power consumers in the system must be represented as
libary PCAs. The Wi-Fi PCA is a ﬁrst example of such library components.
Furthermore, Android application is implemented as a subclass of Activity.
Its behavior is expressed in terms of state-transition system of the life-cycle
implemented by a set of callback methods. Such behavioral speciﬁcation can be
captured by PCA. Thus, the model-based analysis with PCA can be useful for
the design-level checking of ebugs in Android applications.
Android smartphones are equipped with ARM core processors to have the
dynamic voltage-frequency scaling (DVFS). The DVFS governor in Android
changes the voltages and frequencies based on the CPU usage, and has im-
pact on the CPU power consumption and the execution time of a program as
well. The CPU usage is related to the number of active processes, which is not
known beforehand. The power consumption aﬀected by the DVFS may be con-
sidered probabilistic. Therefore, the behavioral analysis of the PCA may need
the stochastic model-checking method [17].

5 Related Work
A. Pathak et al recognized the importance of eliminating energy bugs in smart-
phones, which they called ebugs [14]. They also proposed to use the state-
transition systems for modeling of the power consumption and developed Eprof
[15]. Eprof is an energy proﬁler to monitor the program execution at runtime to
detect potential ebugs.
MoVES [6] uses the UPPAAL/SWA for modeling and analyzing embedded
systems such as the schedulability or the power consumption. The power con-
sumption model, however, is that P (t) = C×t without considering the diﬀerences
in power states. C. Thompson et al [16] presented a model-driven approach to de-
velop smartphone applications. The power consumption analysis was performed
on the generated program codes. The quantitative results reproduced the im-
plemented programs. They, however, did not discuss the formal analysis at the
design level.

6 Conclusion
The power consumption model (Section 2.3) assumes that P (t) is linear in time.
It is one of the future work to ensure that the approximation can mostly re-
produce the energy proﬁle in Figure 2. It requires a measurement by using the
energy proﬁlers such as Eprof.
We compared two approaches to the representation and analysis of the power
consumption automaton using UPPAAL and Realtime Maude. Further feasibil-
ity study is planned to use HyTech [10]. Since the power consumption problem
has some aspects that are hard to predict, such as the eﬀects by the DVFS gov-
ernor, some stochastic analysis methods would be valuable. It is an important
research topic from both theoretical and practical perspectives (Section 4.4).

References
1. Android. http://developer.android.com.
2. Realtime Maude. http://heim.ifi.uio.no/peterol/RealTimeMaude/.
3. IEEE Standard 802.11, Wireless LAN Medium Access Control (MAC) and Physical
Layer (PHY) Speciﬁcations , 1999.
4. R. Alur, C. Courcoubetis, N. Halbwachs, T.A. Henzinger, P.-H. Ho, X. Nicollin,
A. Olivero, J. Sifakis, and S. Yovine. The Algorithmic Analysis of Hybrid Systems,
Theor, Comp. Sci., No.138, pp.3-24, 1995.
5. R. Alur, Formal Veriﬁcation of Hybrid Systems, in Proc. EMSOFT’11, pp.273-278,
2011.
6. A. Brekling, M.R. Hansen, and J. Madsen. MoVES – A Framework for Modeling
and Verifying Embedded Systems, In Proc. ICM2009, pp.149-152, 2009.
7. F. Cassez and K.G. Larsen. The Impressive Power of Stopwatches, In Proc. CON-
CUR 2000, pp.138-152, 2000.
8. M. Clavel, F. Duran, S. Eker, O. Lincoln, N. Marti-Oliet, J. Meseguer, and C.
Talcott. All About Maude - A High-Performance Logical Framework, Springer 2007.
9. A. David, J. Illum, K.G. Larsen, and A. Skou. Model-based Framework for Schedu-
lability Analysis Using UPPAAL 4.1, Aalborg University 2009.
10. T.A. Henzinger, P.-H. Ho, H. Wong-Toi. HyTech: A Model Checker for Hybrid
Systems, Software Tools for Technology Transfer, 1:110-122, 1997.
11. J. Manweiler and R.R. Choudhury. Avoiding the Rush Hours: WiFi Energy Man-
agement via Traﬃc Isolation, In Proc. MobiSys’11, 2011.
12. S. Nakajima and Y. Ueda. Power Consumption Analysis of Smartphone Applica-
tions using UPPAAL, In Proc. 1st CPSNA-WIP, 2013.
13. P.C. Olveczky and J. Meseguer. Semantics and Pragmatics of Real-Time Maude,
Higher-Order and Symbolic Computation, vol.20, no.1-2, pp.161-196, 2007.
14. A. Pathak, Y.C. Hu, and M. Zhang. Bootstrapping Energy Debugging on Smart-
phones: A First Look at Energy Bugs in Mobile Devices, In Proc. Hotnets’11,
2011.
15. A. Pathak, Y.C. Hu, and M. Zhang. Fine Grained Energy Accoutning on Smart-
phones with Eprof: Where is the energy spent inside my app?, In Proc. EuroSys’12,
2012.
16. C. Thompson, D. Schmidt, H. Turner, and J. White. Analyzing Mobile Applica-
tion Software Power Consumption via Model-Driven Engineering, In Proc. PECCS
2011, pp.101-113, 2011.
17. P. Zuliani, C. Baier, and E.M. Clarke. Rare-Event Veriﬁcation for Stochastic Hy-
brid Systems, In Proc. HSCC 2012, pp.217-225, 2012.