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.
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 [
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 [
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.
Android Framework / Linux LCD
CPU(DVFS)
Network
Peripheral
Ba!ery
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 profile of a Wi-Fi client in Nexus One operating in the power save mode
(PSM) [
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 transferring data. Figure 2 shows that the STA is first in the Deep Sleep state, and Power (mW) 500
Beacon 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 flag 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 [
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 suffice 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 funtion of time. Let P (tS , tE )P S be the consumed power in the state P S from tS to tE that P (tS , tE )P S =CP S ×(tE − tS ) with a constant CP S . P (T ) becomes a sum of the power consumptions in all the states that the STA transition system visits.
N−1 ∑ i=0 P (T ) =
P (ti, ti+1)P S where t0 = 0 and tN = T . P (tS , tE )P S can be written as P (t)P S , equal to CP S ×t, with t = tE − tS . For example, P (t)DeepSleep refers to the sum of the 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.
Model-Based Analysis of Power Consumption
We introduce a state transition system, power consumption automaton1, to be a
formal representation. Power consumption automaton (PCA) is a 6-tuple, whose
definition follows the presentation in [
ψ ⇒ { 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 flow dynamics. Act(l) is a differential equation of the form dP/dt = K with K∈Z. K is Cl 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 defined by a linear formula ϕ over V ar.
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) [
The algorithmic analysis methods were studied for linear hybrid automaton
(LHA), specifically the reachability analysis over infinite state spaces generated
by the labeled transition system (LTS) associated with the LHA [
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 different 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
We assume here a PCA with N power states, each of which consumes different electric power as P (t)j = Cj×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 Cj in the power state j, proceeding at N different rates. P ow accumulates all the consumed power. Alternatively, a PCA is represented as an MTS. We regard each P (t)j to be a skewed clock Xj to change at a fixed rate of Cj. Since Xj changes with time only when the PCA stays on that state j, Xj must be stopped in all the other states. PCA is now a multirate stopwatch automaton, where the total power consumption is calculated such that P ow = ∑jN=−01Xj. PCA is more expressive than either MTS or SWA. Some over-approximation method is needed in the tool-assisted analysis.
Init
/ n:=0;
lock:= false
release [ n== 1]
/ n--; lock := false
release
[n> 1]
/ n--;
release
Unlock
Lock
excep!on
This section presents two methods of representing and analyzing the PCA with
two automatic tools, UPPAAL [
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 off. The locked Wi-Fi stays in the Idle Listen state even when the data
transfer ends with the no-more-data flag on2.
This subsection sketches how the PCA is encoded in the stopwatch-extension of
UPPAAL [
Let XP S be a clock variable introduced for a power state P S. We add invariants 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 first-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.
Realtime Maude Realtime Maude [
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 fired 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 } nondeterministically. 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 fire transitions at some time so long as the side condition is satisfied. The transition is fired at least once in the time interval that mte(T ) specifies. Two functions, mte and δ, are defined for each term T .
Realtime Maude supports the timed model-checking of the property expressed 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 behavior 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 consumption, a Boolean flag Bool for the WifiLock 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 flags.
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 first 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 + CHP ×τ, B, X) δ(wif iST A(LightSleep, P, B, X), τ )
= wif iST A(LightSleep, P + CLS×τ, B, X + τ ) if X < C − τ δ(wif iST A(LightSleep, P, B, X), τ )
= wif iST A(DeepSleep, P + CLS×τ, B, X + τ ) if X ≥ C − τ The inactivity timer is time-dependent component in wif iST A. mte is defined 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
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 restriction 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 different 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 first 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 specification 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
impact 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 affected by the DVFS may be
considered probabilistic. Therefore, the behavioral analysis of the PCA may need
the stochastic model-checking method [
A. Pathak et al recognized the importance of eliminating energy bugs in
smartphones, which they called ebugs [
MoVES [
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 reproduce the energy profile in Figure 2. It requires a measurement by using the energy profilers such as Eprof.
We compared two approaches to the representation and analysis of the power
consumption automaton using UPPAAL and Realtime Maude. Further
feasibility study is planned to use HyTech [