日本ソフトウェア科学会第 32 回大会 (2015 年度) 講演論文集

アンドロイド・アプリの電力消費振舞い：
形式モデルと有界解析
中島 震
電力バグを開発上流工程で除去するモデルベース解析の方法を論じる．電力消費振舞いを重み付き時間オートマトンに基づく形式モデル PCA で表す．消費電力解析は有界区間でのコスト制約問題と考えることができ，さらに，ロジック・モデル検査の問題と定式化することができる．本稿では，SAT/SMT ベースのスコープ有界検証を PCAに適用する方法ならびに，この検証作業によって不具合があるとわかった PCA を対象に欠陥箇所を自動特定する方法を提案する．

や消費電力量といった連続値を扱う．CPS の 3 つの1 はじめに特徴

Cyber-Physical System (CPS) （ [13] p.5）というイブリッド性を持つ．実際，線型ハイブリッド・オー

言葉が登場して久しい．その間に普及したスマート

トマトン [6] のサブクラスを採用する研究がみられる

フォンやタブレットといった携帯端末は日常の生活ス[9] [17] [18] [19]．

[30] のひとつである「離散と連続の共存」，ハ

タイルを変えた．組込み装置はネットワークによって電力バグを検知する方法は，消費電力値が予め決

つながり「スマート」なサービスを提供する基盤とめた上限を超えないことを確認すれば良いだろう．となっている．携帯端末や組込み装置の形や機能は千差

ころが，消費電力は時間に対して単調増加するので，

万別な一方，電力消費が大きな問題となるという共計測時間を長くとると，いつの時点かでは必ず上限値

通点がみられる．たとえば，スマートフォンは自身のを超える．計測時間を有界区間に限定することで期待電池で作動する．電池容量は限定されており，充電しする検査が可能になる．積算消費電力量を一般化してない限り電池は減る一方である．また，意図通りの機連続値で表せる数値的なコストとみなすと，これは能を示すアプリケーション・プログラムが予想外の電「有界区間でのコスト制約問題」となる．時間有界の池消耗を引き起こすという「電力バグ (e-bugs)」 [25]到達性解析 [22] や凍結演算子を持つ線型時相論理に対が頻発していることも事実であろう．

するモデル検査の方法を用いれば良い [19] [21]．

モデルベース解析による電力バグ検知の方法があ

このような解析法は，電力バグがあるか否かを自る (例えば [17])．アプリケーション・プログラムから動的に調べ不具合状況を表す反例が出力する．反例

ハードウェアまでを含む全体の電力消費振舞いを統を分析して欠陥箇所をつきとめる作業は多くの工数一的に表現し解析することで，電力バグを検知する ．

を要するので，欠陥箇所を自動的に発見したい．AI

プログラムが示す離散的な振舞いと同時に，実行時間

研究の分野で始まった「モデルベース診断」 [26] を基に，SAT ベースの有界モデル検査法 [7] で用いられEnergy Consumption Behavior of Android Applications : Model and Analysis.
Shin Nakajima, 国立情報学研究所, National Instituteof Informatics.
総合研究大学院大学 SOKENDAIる「振舞いの論理式表現」を組み合わせる方法がある．欠陥箇所自動発見の方法が VLSI デザイン [27] や
手続き型プログラム [12] に適用されて成功している．
本稿では，電力消費振舞いのモデルベース解析法を紹介する．アンドロイド・フレームワークで生じる電2. 2 アクティビティ

力バグの問題を具体例として，電力消費振舞いの形式

アプリはアプリケーション・プログラムであるが，モデル，有界解析ならびに欠陥箇所自動発見の方法を

画面を占有し GUI 部品を通して，利用者とインタラ

述べる．

クションするという特徴がある．GUI インタラクショ
ンはアクティビティと呼ぶコールバック型の処理機構

2 電力バグとモデルベース解析

で実現されている．つまり，アプリの GUI を担うメ

2. 1 アンドロイド多層アーキテクチャ

インスレッドはアクティビティ・オブジェクトを実行

アンドロイド・フレームワーク（あるいは、アンする．

ドロイド） [1] は，リアルタイム・リナックス上に構

アンドロイド・フレームワークは，アクティビティ

築された Java ベースのアプリケーション・フレーム
ワークである†1 ．スマートフォンは，LCD ディスプの生成から消滅までのライフサイクル・ステージごレィをはじめとして，Wi-Fi，GPS 等のさまざまな機

ろが，消滅に関わる振舞いに大きな特徴があり，これ

能ハードウェアを持つ．これらのハードウェア資源はが，さらに電力バグの原因となることがある．アクリアルタイム・リナックスの管理下におかれている．

ティビティが消滅する際，適切な終了処理を実行すアプリケーション，いわゆるアプリは，Java で記述るのが普通のことであり，この処理を行うコールバッ

されたプログラムであって，アンドロイドが提供する

ク・メソッドが定義されている．多くの計算システ

API（オブジェクト群）を通して機能ハードウェア資ムでは，ここで処理漏れがあっても，アプリケーショ

源を使用する軽い糊付けスクリプトである．

ン・プログラムを実行していたプロセスの消滅と共とに適切なコールバック・メソッドを起動する．とこ

アンドロイドは電池消耗を抑えることを目的としに，計算資源が解放される．ところが，アンドロイドて，「積極的な電力削減」ポリシーを採用している．電では事情が異なる．同じアプリが近い将来ふたたび起

池消耗に最も大きく関わる機能ハードウェアは LCD

動される可能性を想定する．引き続く実行開始処理

ディスプレイである．利用者がしばらくの間，画面をを高速化する目的で，消滅したアクティビティのメモ

タッチしないでいるとスリープ・モードに移行する．

リ・イメージを残しておく．メモリ不足が生じた時にLCD ディスプレイを使わないことで電池の消耗を防漸くメモりが上書きされる．消滅したアクティビティ

ぐ．一方，アプリの機能によってはスリープを抑止しの残像中に，電力制御に関わるオブジェクトが生き続

たいこともある．たとえば，ストリームデータの配信

けていると，予想外に電池が消耗される結果となる．

では，利用者は映像を観ているだけであり，画面に働きかけない．画面タッチがないからといってスリープ

2. 3 電力バグの発見していては，映像表示という機能が果たせない．そこ

現在，電力バグの発見には，プログラムを実行してで，アンドロイドは，この基本的なポリシーを上書き

電力消費量を監視するプロファイラ (例えば [25]) がする電力制御 API (Wake Lock) を提供する．Wake

用いられている．ところが，プロファイラはプログラ

Lock を獲得することで，スリープ・モードへの移行

ムの動的テストと同様に，与えたテストデータあるいを禁止する．ところが，このような API を誤使用しは設定したテスト環境のもとでの振舞いを調べるだけている場合，不必要に長い時間にわたって機能ハードであって，網羅的な検査ができない．さらに，アプリウェアを使用することになり，結果として，電池の消の機能は，アンドロイド・フレームワークとリアルタ

耗が予想外に大きくなる．

イム・リナックスを含む全体によって実現される．電力消費するエンティティは，プログラムではなくハー†1 フレームワークとリアルタイム・リナックスの両方を合わせて，アンドロイド・オペレーティングシステムと呼ぶこともある．

ドウェアである．一方，プロセッサならびにメモリといった基本ハードウェア以外の機能ハードウェア・コ
ンポーネントは，アプリが提供する機能に依存して使

用・不使用が決まる．つまり，機能ハードウェアの消費電力はそれを使用するアプリの振舞いに依存する．
電力バグはアプリの振舞いに起因するが，消費電力に関わる不具合は機能ハードウェアの電力消費状態と

beacon[not TIM]

beacon[not TIM]
Deep
Sleep

次に，アンドロイド端末のプロセッサに目を移す．
ハードウェアの点でも省電力を考えることから，DVFS

Idle Listen

Authen!ca!on
Associa!on

ことから，プロファイラ開発にはアンドロイド・オペ
レーティングシステムの改造を伴う（例えば [31]）．

Data transfer[more]

Beacon[TIM]

beacon[TIM]

して認識される．そこで，フレームワークならびにリナックスの内部まで処理の流れを追跡する必要がある

Data transfer[not more]/ reset inac!vity !merHigh Powerbeacon
[TIM]
Light
Sleep

beacon[not TIM]

expire inac!vity !mer

図1

Wi-Fi STA の振舞い

（例えば [11]）による電力制御が可能なプロセッサを採用する．また，マルチコアプロセッサを利用するこ

3. 1 Mealy マシン

とも多い．実行負荷が小さい時は，少ないコア数で低プログラムが示す離散的な機能振舞いのデザイン

い周波数によって実行する．負荷が高まると共に，動表現として，状態遷移システムを用いる方法が知ら

作周波数を上げる，あるいはコア数を増やす，等で負れている（例えば [29]）．オブジェクト指向モデリン

荷上昇に対応する．実行コア個数も動作周波数もプログで用いる UML ステートダイアグラムなどがある．

セッサの消費電力に影響する．

先に述べたように，アプリのアクティビティはアンド

実際の測定実験によると，負荷が大きくなるにつれ

ロイド・フレームワークが規定するライフサイクルにてアプリケーション・プログラムが処理完了するまでしたがって作動する．ライフサイクルは，コールバッの実行時間が長くなり，したがって機能ハードウェア

ク・メソッドの実行と完了をイベントとする Mealy

を利用している場合に消費電力が増大することがわ

マシンで表すことができる [22]．

かる．一方，DVFS によって実行時間をほぼ一定に保つことが可能な負荷領域も存在する．それでも消費

3. 2 Wi-Fi サブシステム

電力のゆらぎが約 30%に達する [20]．つまり，電力

次に，機能ハードウェアの機能振舞いを考える．ア

バグによる影響が消費電力の 30%内であれば，測定

ンドロイド・タブレットの Wi-Fi サブシステム (Wi-Fiのゆらぎに隠れてしまう．プロファイラがアプリ実行

STA あるいは STA) を対象として，Wi-Fi アクセスの際の実測に依存していることの限界を示している．

ポイント (AP) と通信している状況での消費電力の以上から，開発の上流工程で電力消費の振舞い解変化を測定した結果が報告されている [15]．この測定析を行うモデルベース解析方法 [17] への関心が高まっ

結果と IEEE 802.11 標準勧告 [2] で示されている機てきた．次節以降で，モデルベース解析の方法を紹介

能定義から，STA の振舞いを 4 つの状態間を遷移すする．

る状態遷移システム（図 1）として定式化することができる [17]．

3 振舞い表現

Wi-Fi AP は周期的に生成する beacon 信号を使っモデルベース解析はアプリから機能ハードウェアまて，STA にデータ転送の開始を通知する．STA の初期でを含む全体の電力消費振舞いを統一的に表現し解状態は DeepSleep であり，データフレームの送受を析することで，電力バグを検知する方法である．本研行う時には HighPower に遷移する．状態 IdleListen

究では，電力消費振舞いの形式表現として，線型ハイで引き続くデータフレームの到着を待つ．フレーム中

ブリッド・オートマトン [6] を用いることを考える．

に no-more-data フラッグが設定されていると転送終了を示すので LightSleep に遷移する．この状態でSTA は近い将来に開始される新たなデータ転送に備え，DeepSleep 状態には遷移しない．その代わりに，

らびに遷移に付加することができる．本研究での電力タイマーを用い，タイムアウトによって DeepSleep 状

消費振舞いでは，機能ハードウェアの状態遷移は瞬時態に遷移するように制御する．ここで，DeepSleep はに起こると仮定し，重みの更新式を遷移に与えない．

beacon 信号を受信するだけで良いので，使用する電子

一方，クロック変数や重み変数以外の内部状態変数を回路を駆動する小さい電力で良い．一方，HighPower

導入することで，記述の表現力を向上させることがで状態ではデータフレームの中身を調べる必要がある

きる．そこで，このような形式モデルを電力消費オー

ことから大きな電力を消費する．つまり，4 つの状態

トマトン (PCA) と定義した．

は異なる電力消費率を持つ．

検査対象の全体は，アプリならびに機能ハードウェℓ

アから構成される．さらに，補助的なオブジェクトもとする線型近似を導入すると，この状態遷移システ

導入する必要があるだろう．そこで，PCA は並行合

ムは線型ハイブリッド・オートマトン (LHA) で表す

成できなければならない．WTA と同様に共通するアことが可能になる [17]．ある状態に滞留する時間を t

ルファベットに同期して遷移を起こす同期積の方法をとする時，消費電力は M ×t で表され，連続値（実採用する [19]．

状態 ℓ での単位時間あたりの消費電力量を定数 Mℓ数）をとる．状態遷移が続く場合を考えると，初期状態から N 回の遷移についての総和をとればよく，

E=

∑N

j=0

Mj ×tj である．なお，定数 M ℓ は状態 ℓでの平均値とすれば良くハードウェアの諸元から決まる．

4 検査する性質
4. 1 有界区間のコスト制約問題
次に消費電力量に対する検査性質を考える．単純に考えると，消費電力の総和 E が与えられた上限値

Cmax を超えないことと表せる．この性質は線型時相
3. 3 線型ハイブリッド・オートマトン

論理 (LTL) を用いると 2(E ≤ Cmax ) と書ける．し上記の消費電力モデルは線型ハイブリッド・オート

かし，消費電力は積算値であって，機能ハードウェア

マトンで表現可能であるが，そのサブクラスを用いる部品が使用されている時間に比例して増加する．つま研究が知られている．ストップウォッチ・オートマト

り，E の値は時間に対して単調増加するので，Cmaxンを用いる方法 [9] は状態 ℓ ごとの定数値の違いを考が有限値であることから，この単純な性質は，ある

慮しないで全て同じ値とする場合に相当する．異な

時点で満たされなくなる．検査する時間区間を限定ℓ

る M 値を表すにはマルチレート時間システム [18]しなければならない．検査対象の時区間を [ts , te ] とが必要になる．一方，消費電力の表現を考える際にすると，∀t∈[ts , te ] | E(t) ≤ Cmax であろう．一方，は，これよりも簡単な形式モデルである重み付き時間

検査対象は状態遷移系の一種であることから，対象

オートマトン (WTA) で良い [19]．消費電力 E は時の振舞いは遷移する状態の列で表される．明示的に間経過と共に積算され，検査時に値が必要になるだけ

時間情報を用いる区間を指定することは難しい．しであり，状態遷移エッジのガード条件等に現れることたがって，状態を用いて区間を指定することが望まはない．つまり，E は観測可能な値であれば良く，積しい．∀σ∈[σs , σe ] | E(σ) ≤ Cmax である．なお，指極的に状態遷移の振舞い制御に関わらない．そこで，定区間内で新たに生じた消費電力量を検査する場合

時間オートマトン (TA) [4] の拡張である WTA [3] をは，∀σ∈[σs , σe ] | (E(σ) − E(σs )) ≤ Cmax である．

用いて表現する．

E(σs ) = 0 とすれば上記と同じ形の式になる．

以上から，アプリならびに機能ハードウェアの双方

以下では，これを一般化して考える．コスト制約をを状態遷移マシンで表すことにする．一般に，Mealy

実数上の線型不等式とする時、「有界区間におけるコマシンは WTA の特殊形になる．つまり，Mealy マ

スト制約問題」と呼ぶ．コスト制約として，クロック

シンを，クロック変数なし，重みなしの特殊形と考え変数や重み変数（消費電力の積算値）に対する数値制れば良い．なお，WTA では，重み値更新式を状態な約を考えれば良い．

検査性質を具体的に議論するには，有界区間の指定

4. 3 時間有界探索

方法とコスト制約の表現方法を考える必要がある．電

第 2 に，有界な区間での検査に限定すれば良いこ

力消費の振舞いが状態遷移システムで表されることかとから，fWLTL 式を使う場合に比べて簡便な方法もら，区間の開始と終了を状態で印付けすれば良いだろ

考えることができる．検査対象 PCA が生成可能な経う．今，Ps ，Pe を状態命題とする時，LTL を用いて，路の全体から特定の性質を満たす経路だけを選び出Ps ∧ 3Pe の形で表せる．一方，コスト制約はクロッ

し，その選んだ経路についてのみ，コスト制約を評価

ク変数や重み変数に対する線型不等式である．命題

する．クロック変数および重み変数を凍結する状態を

Pj が成り立つ状態でのクロック変数の値を Xj ，重み

何らかの方法で別途指定する．今，選び出す経路の条

変数の値を Wj とする時，コスト制約 C⟨C x ;C w ⟩(s, e)

件をガイド制約 φG で表す時，検査対象 PCA A に対x

は (Xe − Xs ≤C )∧(We − Ws ≤C ) のように表現でして，A |= φG ⇒ C ⟨C ;Cきる．そこで，Xj および Wj の読み出し方法を具体

当する．

x

w

的に考えれば良い．いくつかの方法が考えられる．

w⟩(s, e) を調べることに相先の fWLTL の場合では，クロック変数および重み変数を凍結する状態の指定方法が明確であった．一4. 2 ロジック・モデル検査

方，この方法では，検査対象の PCA 中に明示的に書第 1 に，凍結限量子を LTL に導入する方法がある

き表す必要がある．コスト制約として，冒頭の簡単な[19]．この fWLTL と呼ぶ体系は，TPTL [5] を基に凍結限量する変数値をクロック変数および重み変数と性質 2(E ≤ Cmax ) に限定する場合に有効な方法である†2 ．文献 [22] では，Real-Time Maude の時間有する拡張である．ϕx を変数 x が自由出現する LTL

界横型探索の方法を用いた実験例が報告されている．

x.ϕx によって，限量変数F式とする時，TPTL では

x に ϕx が成り立つ状態での時点値を束縛（凍結）す5 スコープ有界検証

る．fWLTL では限量子に注釈を与えるように拡張

5. 1 有界モデル検査の問題

m

x

F

x.ϕ によって，m で指定されるクロック変数

一般に，ロジック・モデル検査や状態空間探索によあるいは重み変数の値を凍結するようにした．なお，

る自動検証の方法では，いわゆる「状態空間の爆発」

LPTL の凍結限量子は時点 τ を明示して

τ

F

し，

x.ϕx とすれば良い．fWLTL を用いると，先の性質は，

u.(Ps ∧
F

F

3

X

y.

されたのが，SAT 法を用いる有界モデル検査 (BMC)である [7]．検査対象システムの実行可能な経路の全

W

F

x.

W

F

X

という問題が生じる．これに対する解決策として提案

v.(Pe ∧ C

⟨C x ;C w ⟩(s, e)))

体を（命題）論理式 φT F にエンコードする．この時，のように書く．その結果，消費電力の解析問題を，遷移列の経路は有限長に限定する．検査性質を表す表

fWLTL 式の PCA に対するロジック・モデル検査と

明 φAS に対して，BMC 問題は ¬(φT F ⇒ φAS ) のして定式化できる．

充足性判定になる．この論理式全体が充足する時，命ところが，fWLTL は TPTL を含む一方，TPTL

題変数値の割当て（モデル）は，φT F が φAS 満たさ

は MTL を含むことが知られている．MTL (Metric

ない理由（反例）を表す．歴史的な経緯から BMC と

Temporal Logic) 式の TA に対するロジック・モデ

呼ばれるが，以下，最近の呼び方にしたがって，ス

ル検査は一般の連続時間に対して決定不能である．

コープ有界検証と呼ぶ．

PCA が TA の拡張であることを考慮すると，fWLTL

検査式 φAS を，前節と同様に，2ψ に限定する場合と PCA に関するロジック・モデル検査も一般には決について，もう少し詳しく説明する．検査対象 PCA

定不能である．そこで，文献 [21] では，近似手法を導の状態を表現する変数の集合を U とする．U j を添字

入し，さらに検査 fWLTL 式のパターンを限定して，

j で区別する集合とする．特に初期状態は U 0 である．

Real-Time Maude [24] の LTL モデル検査に翻訳する方法を採用した．

†2 ただし有界区間に限定．

論理式 φT S は初期状態から K ステップでの遷移全

transfer

体を表す．初期状態を定義する論理式を I ，遷移関係
jを T ，T (Uj−1j, U ) を状態 U

j−1

finish [ locked ]transferjから U への遷移012関係とする．この時，K ステップ遷移は

φT F =I(U 0 ) ∧ (∧j=1..K[ timer >= Expire]

T j (U j−1 , U j ))finish [ not locked ]/ timer := 0transferとなる．次に，¬(φT F ⇒ φAS )= φT F ∧ ¬φAS であることを利用する．2ψ の否定は 3¬ψ であり，K ス
テップの範囲で，3¬ψ=∨

j=1..K

unlock / locked := false

lock / locked := true¬ψ(U j ) である．し

図2

PCA の例

たがって，スコープ有界検証の方法は，次の論理式

φsaf ety の充足性判定問題になる．
φsaf ety =I(U ) ∧ (0∧jj=1..K

T (U

∨

∧(

[ Xs >= C2’ ]/ transfer; Xs := 0

/ lock; Xc := 0j−1j, U ))

j=1..k¬ψ(U j ))5. 2 PCA の有界区間解析
スコープ有界検証の方法を導入するには，検査対01[ Xc >= C1’ ]/ unlock

図3{ Xc =< C1 }0

1

{ Xs =< C2 }{ Xs =< C3 }[ Xs >= C3’ ]/ finish; Xs := 0

Client（左側）と Wi-Fi AP（右側）

象の φT F ，つまり遷移関係の論理式表現を定義しな

本 稿 で 行 う 解 析 は ，有 界 区 間 で の こ コ ス ト 制 約ければならない．PCA は TA の拡張であることから，

問 題 で あ り，ガ イ ド 制 約 φG を 用 い る ．こ れ は ，TA に対する遷移関係定義 [28] をもとにした方法を適φT F ∧¬(φG ⇒φAS ) であり，(φT F ∧φG )∧¬φAS の形用すれば良い．

のスコープ有界検証問題である．

PCA は，離散遷移と時間遷移という 2 種類の遷移を持ち，これらの論理式表現を考える [23]．状態を

5. 3 例表す変数 U を act（イベント記号），at（ロケーショ

図 2 に示した簡単な例を考える．これは，図 1 をン），x（クロック変数），w（重み変数），v（内部変単純化した W-Fi STA の PCA であり，3 つの状態数）からなるとする．

からなる．状態 ℓ0 は deep-sleep を表し，ここでの単a,g,r,u ′状態 ℓ から ℓ への遷移を e = ℓ −→ ℓ とする．こ位時間あたりの消費電力 (M 0 ) は小さい．状態 ℓ1 のこで，a はイベントを表すアルファベット，g はガー

light-sleep では，その値は M1 は M 0 よりも大きい．

ド条件，r はリセットクロックの集まり，u は内部状

一方，状態 ℓ2 ではデータフレームのデコード処理を態の更新処理，を表す．この時，遷移 e に対する離散行うので最も大きな値 M2 ) を持つ．状態遷移の図か

遷移の論理式表現 T (e) は次のように定義できる．

ら，Lock されていない時，データフレーム転送終了

′

′

′

T (e) = (at = ℓ∧at = ℓ ∧act = a∧g∧x = z
′

′

′

′

∧w = w∧v = f (v)∧Inv(ℓ )(x ))と共に、状態 ℓ2 から ℓ1 へ遷移する．この時，タイム
アウトで ℓ1 から ℓ0 へ遷移するようにタイマーを設

Inv(ℓ) は状態 ℓ のクロック不変式，f ∈u は値更新関定する. 逆に，Lock されている時，転送が終了して数である．

も，状態 ℓ2 に留まる．

時間遷移は，δ を適切な経過時間を示す正の実数と次に，図 3 に示した Client と Wi-Fi AP からなる

して，論理式表現 D(δ, ℓ) を次のように定義する．こ全系のシナリオを考える．文献 [22] の例題を簡単化しこで，時間遷移を表す特別なアルファベット delay をたものに相当する．消費電力の総和 E が最大値 Cmax用いた．

以下であるという簡単な検査性質を考える．先に論じ′′D(δ, ℓ) = (at = at∧act = delay∧x = x + δ
′

′

′

′

∧w = w + M ×δ∧v = v∧Inv(ℓ )(x ))ℓた ∀σ∈[σs , σe ] | E(σ) ≤ Cmax である．LTL の論理式

φAS = 2(E ≤ Cmax ) で表現できる．また，検査対象として，lock で始まり，finish を経て， transfer

Client

Wi-Fi AP

Wi-Fi STA
lock

6 欠陥箇所特定

02transfer

6. 1 モデルベース診断

finish

先に述べたようにスコープ有界検証は論理式

φBM C の 充 足 性 判 定 問 題 に 帰 着 さ れ る ．こ こ で ，

d6

φBM C = (φT F ∧φG )∧¬φAS である．反例が生成さ

transfer

れる場合，その反例，あるいは反例に含まれる情報
図4であって φAS を満たさないことを表す最小の情報を反例のメッセージ列

で終わる区間を考え，これをガイド制約 φG として

エンコードした論理式を φT F とする時，充足不能とをφとする†4 ．論理式 φなる論理式 φ ∧φ表す．つまり，φG =lock∧3(finish∧3transfer)が充足不能な時，その充足不能コアに欠陥箇所が含まで，状態 σs として lock 実行後を考え，E(σs ) = 0

れる．

TF

AS

FL

FL

としていることに相当する．この時，スコープ有界

欠陥箇所自動特定の系統的な枠組みとしては「モ検証の問題は，¬φAS =3(E > Cmax ) であるから，

デルベース診断 (MBD)」 [26] がある．MBD では充

φT F ∧ φG ∧ 3(E > Cmax ) になる．ここで，論理

足不能な論理式 φF L の充足不能コアを conflicts と式 φT F は 3 つのオートマトンを並行結合した全系が呼ぶ．一方，φF L の構成部分式の一部を除去するこ生成する遷移系列の全体を表す．

とで，φF L が充足させることができる．この除去す実際の実験では，クロック制約 (C1 , C2 , and C3 ),る部分が欠陥箇所であり，diagnoses と呼ぶ．形式的ガード条件 (C ′ 1 , C ′ 2 , and C ′ 3 ), および検査性質には conflicts は φF L の MUSes であり，diagnoses(Cmax ) 等の定数に具体的な値を与える. 特に，C2 とは MCSes である．ここで，MUSes は MUS(Minimal′

C 2 を大きな値にすることで，Wi-Fi STA (図 2) がUnsatisfied Subset) の集合，MCSes は MCS (Min-

Lock されている時に検査性質が満たされなくなる状

imal Correction Subset) の集合（例えば [8])．また，況を作った．

MCSes と MUSes はヒッティングセット関係で結ば

具体的な値 K を選んでスコープ有界検証を行う†3 と 反 例 が 生 成 さ れ て ，(lock, δ ,transfer, δ ,れている．MCSes あるいは MUSes を求めれば良い．

finish, δ6 ,transfer) を得る．

る方法を採用する [14]．

24

本稿では，MCSes を MaxSAT 問題の解として求め

図 4 はメッセージ系列図として表現した．3 つのオー

論理式 φF L が充足不能な時，MaxSAT 問題は，充トマトンは並行実行されるので，このメッセージ列

足する部分式の個数が最大になるように除去する部

は，検査性質を満たさないインターリーブのひとつに分式を求める．また，論理式 φF L から MCSes を求なる．Wi-Fi STA は初期状態 ℓ0 にいるが，transfer

める際，φAS は除去部分式の対象にしたくない．そによって状態 ℓ2 に遷移する．その後，finish がある

こで，Partial MaxSAT (pMaxSAT) 問題を用いる．

にも関わらず，Lock されているので，同じ状態に留部分式ごとに，soft あるいは hard を指定する．この′まる．d6 時間経過後，transfer があり，d6 ≥C 2 を時，pMaxSAT 問題は，すべての hard 部分式を満た満たす．C ′ 2 の値を大きくとったことから，この時点

すと同時に，満たす soft 部分式の個数が最大になる

での電力消費の総和 E は検査条件を満たさない．E

ように，つまり，除去する soft 部分式の個数が最小は M0 ×d2 + M2 ×d4 + M2 ×d6 である．

になるように選ぶ．この方法を採用すると，φAS を

hard にする．さらに，削除の候補となる φT F についても，欠陥候補としたくない部分式を hard にし，候†3 Yices-1 [10] を利用．
†4 ここで，φT F は反例なので φG を考慮済みである．

補としたい部分式を soft とすれば良い．何を soft と

よって MCS を網羅的に求める．Wi-Fi AP (図 3 右するかは，想定している「故障モデル」に依存する．

側) の要素に関連した 2 つの MCS からなる MCSes{{[Xs≥C ′ 2 ] on ℓ0 →ℓ1 }, {(Xs := 0) on ℓ1 →ℓ0 }} を得た.

6. 2 PCA の欠陥箇所特定方式
PCA を対象として欠陥箇所特定を自動化するには，最初の MCS {[Xs≥C ′ 2 ] on ℓ0 →ℓ1 } は finish と検査対象の振舞いを表す論理式表現，検査性質に加えその後の transfer の間の時間 C ′ 2 が大きいことを示て，故障モデルを決める必要がある [23]．故障モデル

す．Wi-Fi STA は，finish 後に状態 ℓ2 で transferは検査したい性質に合わせて考えるので，本稿で扱っを待っており，この経過時間が大きいと多くの電力をている消費電力の問題を振り返る．

消費する．つまり，C ′ 2 を小さくすれば良い．

∑N

Mj ×tj で表される総消費電力 E に対して，

2 つめの MCS {(Xs := 0) on ℓ1 →ℓ0 } を参照する

検査式を 2(E ≤ Cmax ) とした．Mj は定数なので，と，クロック変数 Xs を 0 よりも大きな値に初期化す

結局，この性質は経過時間 tj に依存する．ti−1 かられば状態 ℓ0 から ℓ1 へのエッジ上のガード条件が，よ

ti のような経過時間の区切りは離散遷移が起こす．

り短い経過時間で発火するようにできることを示唆し

一方，PCA の定義から，状態遷移列の時間経過にている．ところが，PCA の定義から，クロック変数

影響を与えるのは，状態に付された不変式，遷移エッに任意の値を設定することはできない．単に，リセッ

ジ上のガード条件およりリセット条件である．つまトするだけである．つまり，この２つめの MCS は見り，ある遷移列に対して，上記の検査式が満たされる

かけの欠陥箇所であって，除去可能な原因ではない．

j=0か否かは，その遷移列上のクロッック変数に関わる制
約条件との関係で決まる．そこで，本稿の故障モデル

7 むすびを，これらクロック変数に関連する制約条件の出現箇

アンドロイド・アプリの消費電力振舞いを対象としH所から構成する．以下，pという表記は，p が hard

たモデルベース解析の方法を紹介した．PCA と呼ぶ

S

重み付き時間オートマトンが中心的な形式モデルでであることを示す．同様に p は p が soft である．
′

′ H

T (e) = ((at = ℓ) ∧(at = ℓ ) ∧(act = a)HH∧(g)S ∧(x′ = z) ∧(w′ = w)
S

′

H

′

H

制約の問題である．この問題を解くのに，ロジック・′ S∧(v = f (v)) ∧(Inv(ℓ )(x) ) )′ H

モデル検査や時間有界探索の方法があった．本稿でD(δ, ℓ) = ((at = at ) ∧(act = delay)
′

H

′

H

は，SAT/SMT ベースのスコープ有界検証の方法をH

導入し，さらに，欠陥箇所自動特定の方法を述べた．

∧(x = x + δ) ∧(w = w + M ×δ)
′

H

′

ℓ

′

ある．この時，消費電力の解析は有界区間でのコスト

S∧(v = v) ∧(Inv(ℓ )(x )) )PCA 等の形式的な定義の詳細については，関連文献[19] [23] を参照されたし.

今，φT F を決めた時，つまり反例を決めた選んだ時，現状，小さい例題を用いて提案方法の妥当性を確認

この論理式がエンコードしている遷移の列 {→j } から，した段階である．PCA は線型ハイブリッド・オート

クロック変数に関わる部分式を集めて φCLK を作るとマトンのサブクラスでありながら，興味深い応用問題

する．この時，欠陥箇所特定の問題は，φCLK ∧φASに適用できる．サブクラスといっても TA よりも表のクロック制約問題になる．

現力が大きいことから，一般には，自動解析アルゴリ
ズムの複雑さという点で難しい問題が残る．ただし，

6. 3 例

電力消費は有界区間での解析という制限された問題

具体例として前節のスコープ有界検証の例についなので，このことを利用して，複雑さを軽減した解析て欠陥除去の方法を説明する（図 4 参照のこと）．

方法が利用可能といえる．

φT F を反例から構成し，φT F ∧2(E ≤ Cmax ) の論
理式 φF L に対して，pMaxSAT ソルバー Yices-1 に謝辞 本研究は JSPS 科研費 24300010，26330095

の助成を受けたものです．

参 考 文 献[ 1 ] Android. http://developer.android.com.
[ 2 ] IEEE Standard 802.11, Wireless LAN Medium
Access Control (MAC) and Physical Layer (PHY)
Speciﬁcations , 1999.
[ 3 ] R. Alur, C. Courcoubetis, and T.A. Henzinger.
Computing Accumulated Delays in Real-Time System, In Proc. CAV 1993, pp.181-193, 1993.
[ 4 ] R. Alur and D.L. Dill. A Theory of Timed Automata, TCS, 126, pp.183-235, 1994.
[ 5 ] R. Alur and T.A. Henzinger. A Really Temporal Logic, J. Assoc. Comp. Machin., Vol.41, No. 1,
pp.181-204, 1994.
[ 6 ] R. Alur, C. Courcoubetis, N. Halbwachs, T.A.
Henzinger, P.-H. Ho, X. Nicollin, A. Olivero, J.
Sifakis, and S. Yovine. The Algorithmic Analysis ofHybrid Systems, Theor, Comp. Sci., No.138, pp.324, 1995.
[ 7 ] A. Biere, A. Cimatti, E.M. Clarke, and Y. Zhu.
Symbolic Model Checking without BDDs, In Proc.
TACAS 1999, pp.193-207, 1999.
[ 8 ] A. Biere, M. Heule, H. Van Maaren, andT.Walsh (eds.). Handbook of Satisfiability, IOS
Press, 2009.
[ 9 ] A. Brekling, M.R. Hansen, and J. Madsen.
MoVES – A Framework for Modeling and Verifying
Embedded Systems, In Proc. ICM2009, pp.149-152,
2009.
[10] B. Dutertre and L. de Moura. The Yices SMT
Solver. http://yices.csl.sri.com[11] J.L. Hennessy and D.A. Patterson. Computer
Architecture : A Quantitative Approach (5ed.),Morgan Kaufmann 2011.
[12] S. Lamraoui and S. Nakajima. A Formula-based
Approach for Automatic Fault Localization of Imperative Programs. In Proc. ICFEM’14, pp.251-266,
2014.
[13] E.A. Lee and S.A. Seshia. Introduction to Embedded Systems - A Cyber-Physical Systems Approach, LeeSeshia.org, 2011.
[14] M.H. Liﬃton and K.A. Sakallah. Algorithms
for Computing Minimal Unsatisﬁable Subsets ofConstraints. Automated Reasoning, 40(1), pp.1-33,
2008.
[15] J. Manweiler and R.R. Choudhury. Avoiding the
Rush Hours: WiFi Energy Management via Traﬃc
Isolation, In Proc. MobiSys’11, pp.253-266, 2011.

[16] A. Morgado, M. Liﬃton, and J. MarquesSilva. MaxSAT-Based MCS Enumeration. In Proc.
HVC’12, pp.86-101, 2013.
[17] S. Nakajima. Model-based Power Consumption
Analysis of Smartphone Applications, In Proc.
ACES-MB 2013, pp.5:1-5:10, 2013.
[18] S. Nakajima. Everlasting Challenges with the
OBJ Language Family, In Proc. SAS 2014, pp.478493, 2014.
[19] S. Nakajima. Model Checking of Energy Consumption Behavior, In Proc. 1st CSDM Asia, pp.314, 2014.
[20] S. Nakajima and M. Toyoshima. Behavioral Contracts for Energy Consumption, Ada User Journal,
vol.35, no.4, pp.266-271, 2014.
[21] S. Nakajima. Using Real-Time Maude to Model
Check Energy Consumption Behavior, In Proc. FM
2015, pp.378-394, 2015.
[22] S. Nakajima. Formal Analysis of Android Application Behavior with Real-Time Maude, In Proc.
CPSNA 2015, pp.7-12, 2015.
[23] S. Nakajima and S. Lamraoui. Fault Localization of Energy Consumption Behavior using Maximum Satisiﬁability, In Proc. CyPhy 2015, (to appear) 2015.
[24] P.C. Ölveczky and J. Meseguer. Semantics andPragmatics of Real-Time Maude, Higher-Order andSymbolic Computation, vol.20, no.1-2, pp.161-196,
2007.
[25] A. Pathak, Y.C. Hu, and M. Zhang. Bootstrapping Energy Debugging on Smartphones: A First
Look at Energy Bugs in Mobile Devices, In Proc.
Hotnets’11, pp.5:1-5:6, 2011.
[26] R. Reiter. A Theory of Diagnosis from First
Principles. Artificial Intelligence, 32(1), pp.57-95,
1987.
[27] S. Safarpour, H. Mangassarian, A. Veneris, M.H.
Liﬃton, and K.A. Sakallah. Improved Design Debugging using Maximum Satisﬁability, In Proc. FMCAD’07, pp.13-19, 2007.
[28] M. Sorea. Bounded Model Checking for Timed
Automata, ENTCS, 68(5), pp.116-134, 2002.
[29] R.J. Wieringa. Design Methods for Reactive Systems, Morgan Kaufmann Publishers 2003.
[30] J.M. Wing. Cyber-Physical Systems, Computer
Research News, 21(1), p.4, 2009.
[31] L. Zhang, M.S. Gordon, R.P. Dick, Z.M. Mao, P.
Dinda, and L. Yang. ADEL : An Automatic Detector of Energy Leaks for Smartphone Applications,
In Proc. CODES+ISSS’12, pp.363-372, 2012.