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

スマホ・アプリの電力消費振る舞いと検査性質の表現
中島 震

スマホやタブレットのアプリケーションに潜む電力バグを、ソフトウェア開発上流工程で除去することを目的として、モデルベースの電力消費解析技術が関心を集めている。本稿では、電力消費振る舞いを表現する電力消費オート
マトン (PCA) と検査性質を表現する重み線型時相論理 (fWLTL) を提案する。PCA は実数値の重みを持つ時間
オートマトンであり、fWLTL は凍結限量子 (freeze quantifier) によって重み値を参照可能な線型時相論理である。
また、PCA の重みに確率コンポーネントを導入することで確率過程を表現することができ、不確定さを伴う動作環境下での、電力消費振る舞いの表現も可能になる。fWLTL の PCA に対するモデル検査は決定可能でないが、サン
プリング抽象や統計モデル検査の方法を用いれば良い。

を、適切な抽象レベルで表現した「モデル」が中心と

1 はじめになる。文献 [11] は、消費電力という連続量を取り扱う

スマートフォンやタブレットといった携帯端末でハイブリッド・オートマトン [4] による方法を提案しは、電池容量が小さいことから、開発の初期段階かた。WiFi コンポーネントを代表例として、直接の消ら、アプリケーション・プログラムの電力消費に注意

費者となるハードウェア・コンポーネントの電力消費することが期待される。アンドロイド・フレームワー

振る舞いが表せることを示した。一方で、アプリケー

ク [1] は、電力消費を間接的に制御する管理 API を提ションに期待される性質については、ある範囲で電力供している。ところが、このような API の誤使用が、消費量を超えないこと、という素朴な観点が提示さ

電池の消耗が大きくなる「電力バグ (ebugs)」 [17] のれるのみだった。きちんとした議論が行われていな

原因となることがある。現状、電力バグの検知には、かった。

プログラムを実行して使用電力量を監視するプロファ

本稿では、電力消費振る舞いを表現する電力消費

イラ (例えば [18] [20]) が用いられている。プロファイ

オートマトン (PCA) に加えて、検査性質を表現す

ラによる方法は、実行状況に依存する様々な影響を受る重み線型時相論理 (fWLTL) を提案し、PCA に対ける。さらに、本来、設計ミスに起因する不具合でする fWLTL 式のモデル検査法を考察する。ここで、あっても、プログラムを実行してはじめて検知するもPCA は、文献 [11] [12] で採用した形式化と異なり、実のである。そこで、開発上流工程で、アプリケーショ

数値の重みを持つ時間オートマトンとして定義する。

ンの電力消費振る舞いを調べるモデルベース解析のまた、fWLTL は凍結限量子 (freeze quantiﬁer) [3] に

方法 (例えば [11]) が関心を集めるようになってきた。

よって重み値を参照可能な線型時相論理である。

モデルベース解析の方法では、電力消費振る舞い

以下、第２節で電力消費振る舞いの概要を紹介する。第３節と第４節は PCA と fWTLT を導入し、第Behavioral Specification and Properties of Energy
Consumption in Smartphone Applications.
Shin Nakajima, 国立情報学研究所, National Instituteof Informatics.

５節でモデル検査法について考察する。第６節で関連研究との比較を論じ、第７節で今後の課題を整理する。

知する方法として、プロファイラ (例えば [18] [20]) がApp

Service

用いられている。開発済みプログラムを実行し、消費電力の変化を監視する方法である。正確な消費電力量

Android Framework / Linuxを得るには、検査対象プログラムが作動しているス
マホに外部接続した電流メータ等によって測定する。

LCD

CPU (DVFS)

Network

Peripheral

ところが、目的を電力バグの検知に限定すれば、想定外の電力消費があるか否かを調べるだけで良く、正確Ba!eryな数値は不要になる。
プロファイラの検査対象は、アンドロイド・フレー

図1アンドロイド階層アーキテクチャ

ムワークやリナックスのシステム・コードを含むプログラム実行に関わる処理の全体である。このことは、
次のような 2 つの難しさを生じる。第１に、利用者作

2 モデルベースの電力消費解析

成プログラムに潜む電力バグの原因箇所を特定するにスマホ・アプリの電力消費を、アンドロイド・フ

は、アンドロイドやリナックスの内部に監視ポイント

レームワーク [1] を具体例として考える。

を埋め込み、メソッドの呼び出し木 (Call Tree) を追跡する必要がある。つまり、プロファイラ向けフレー

2. 1 アプリケーションの電力消費ムワークを開発しなければならない。第２に、デバッ

アンドロイドはリナックスに統合されたアプリケー

グ対象プログラム以外の機能の影響も受ける。アンション・フレームワークであり、図 1 に示したようなドロイドでは、さまざまなサービスが稼働しており、

階層アーキテクチャになっている。アプリケーション

対象プログラムだけを切り離した環境で実行するこは、Java で作成されたマルチスレッド・プログラムとが困難である。また、直接の電力消費者であるハーで、GUI を持つアプリ (App) あるいはバックグラウ

ドウェア・コンポーネントは、物理的な特性に影響さンドで実行されるサービス (Service) に分類される。

れる。たとえば、WiFi コンポーネントであれば、信フレームワーク提供クラスを通して、LCD、CPU、

号強度に依存して、消費電力が変化する。検査対象のネットワークといったハードウェア・コンポーネント

動作環境に依存した測定のばらつきを避けることがを利用する。これらのコンポーネントは、CPU も含できない。

めて、バッテリーが供給する電力なくしては作動しさらに、プロファイラは、プログラム実行に依存しない。すなわち、ハードウェア・コンポーネントが電た方法であることから、通常のプログラムテストと同力を直接消費するのに対して、アプリケーション・プ

様なカバレッジに関わる問題点が残る。電力バグを示

ログラムはハードウェアの利用者であるという点で、すプログラム実行経路を検査できている保証がない。

間接的な電力消費者である。アンドロイドは、電力制

電力バグの原因が、アプリケーション・プログラムの御に関わる API を提供しており、アプリケーション

電力管理 API 誤用である場合、これは設計段階で除の作り方によって、電池を効果的に使用する工夫が可

去すべき欠陥である。そこで、モデルベースの解析技能になる。一方、このような API の使い方を誤ると、術による電力バグ除去の方法確立が期待されるよう意図通りの機能を果たすプログラムであっても、予想になった。次節で、モデルベース電力消費解析の基礎

外に電池を消耗することがある。このような電力消となる「モデル」について考察する。

費に関わるプログラムの欠陥を「電力バグ (ebugs)」[17] と呼ぶ。電力バグの「真の」原因は、プログラムの作り方にある。
アプリケーション・プログラムに潜む電力バグを検2. 2 電力消費モデルの考え方
2. 2. 1 電力消費振る舞いモデル
アプリケーション・プログラムは、電力に関して間
接的な消費者であり、ハードウェアと一体化した記述

beacon[not TIM]

beacon[not TIM]
Deep
Sleep

電力消費振る舞いを、電力状態と電力状態間の遷移からなる状態遷移システムとして表現する方法を提Idle Listen

Authen!ca!on
Associa!on

ウェア・コンポーネントの電力消費振る舞いを含むモ
デル記述が必要になる。文献 [11] では、このような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

図2

電力消費オートマトンの例

案し、電力消費オートマトン (Power Consumption

Automaton、PCA と略す) と名付けた。
PCA の各状態での単位時間あたりの電力消費量がマトンになる。さらに、消費電力が連続量であることを考慮すると、PCA は、素朴には、ハイブリッド・

与えられているとすると、その状態に留まっていた時

オートマトン [4] になる。

間がわかれば、電力消費量を計算できる。振る舞い仕2. 2. 2 線型近似の導入

様にしたがって状態遷移の列を求め、訪問した状態に

文献 [11] [12] では、電力消費を線型近似した PCA

付与されている値をもとにして電力消費量の総和を計を提案した。実際、WiFi コンポーネントのハード

算すれば、一連の処理で消費した電力量を求めること

ウェア諸元は、各状態での単位時間あたりの消費電力ができる。状態 j での電力消費率を F j (t) とすると、値を定数としている。電力バグ検知を目的とする解析

j

∫b

j

∑an ∫ bj

電力消費は P =

P =

∑n

j=0

P =

j

F (t)dt である。総電力消費は、

j=0

aj

j

F (t)dt である。

図 2 は、WiFi クライアントの PCA のダイアグラ

では、消費電力の正確な値を予測する必要がない。線型近似の方法は、モデルベース解析という目的に合った良い抽象化になる。

ム表現である。WiFi コンポーネントの電力消費振電力状態 ℓ での単位時間あたりの電力消費量を M ℓ

る舞いを示し、PCA の特徴を良く表している。4 つとすると、電力消費を表す変数 P のダイナミックスの電力状態（DeepSleep、HighPower、Idle Listen、は、dP/dt = M ℓ となる。電力消費のない状態が存LightSleep）と、これらの間をつなぐいくつかの遷在することを考慮し、0 を含む整数 (M ℓ ∈ N ) とす

移エッジからなる。初期状態は、DeepSleep であり、る。一方、クロック変数 X の場合は、dX/dt = 1 でデータ転送開始を示す beacon 信号の受信によってあり、変数 P のダイナミックスの特殊な場合に相当

HighPower 状態に遷移する。IdleListen でフレームすることがわかる。

受信待ち・HighPower で受信という一連の処理を繰

ダイナミックスに着目すると、非負の実数値をとる

り返す。データ転送が終了すると、LightSleep に遷

連続変数 Y ∈R+ (dY /dt = M ℓ ) は、LHA の特殊な移する。ここで、新たなデータ転送が開始されると、場合に相当する。ストップウォッチ変数 (dY /dt = 0)

HighPower と IdleListen の遷移を繰り返す。一方、を含む n-レート時間システム (n-rate Timed System)

データ転送が生じない場合、inactivity timer のになる [11]。状態不変量やガード条件の制約式を時間

タイムアウトによって、LightSleep から DeepSleep

オートマトンのクロック変数と同様な線型不等式に限に遷移する。

定しても、到達性解析（reachability）が決定不能で

上記の概略シナリオにあるように、PCA は、状態で電力を消費し、特定の信号受信などのイベントあるあることが知られている [4]。
電力消費変数は、その総和が重要な、観測変数 (ob-

いはタイマーのタイムアウトによって状態遷移を起こ

server)(例えば、 [7]) である。電力消費変数の値が不す。PCA は、タイマーを持つことから、時間オート変量やガード条件に現れるわけではなく、クロック変数がタイムアウト等によって振る舞いに影響を与えは、線型時相論理 (LTL) の式 2(IL⇒3LS) として表ることと比べて大きく異なる。そこで、電力消費変現できる。これに、時間経過に関わる連続量、電力消数を重みにエンコードした重み付き時間オートマト

費を監視する連続量の情報を補えば、検査したい性質

ン [5] [6] として表現する。この時、振る舞いに影響をを表現することができる。クロック変数に関わる条件

与えるのはクロック変数であり、到達性解析は、ダイを表現可能な時相論理の体系として Metric Temporal

ナミックスが dX/dt = 1 の時間オートマトンと同様

Logic (MTL)(例えば [16]) がある。電力消費のようにに、決定可能となる。

クロック変数以外の連続値変数を取り扱うものでは

電力消費変数のダイナミックスは、文献 [13] で考察ない。

したように、確率的な変動を持つ場合がある。この

本稿では、TPTL [3] が導入した凍結限量子 (freeze

場合、確率分布 f (r) に従う一様乱数 R に依存した確

quantiﬁer) を拡張する。凍結限量子を用いて表した
論理式

m

F

率的な値 α(R)(α≥1) を用いて、dP/dt = α(R)×Mℓx . ϕx は、「変数 x が自由出現する論理式と表すことができる。確率的なコンポーネントを重みϕx が充足する状態での変数値 m を x に束縛する」こにエンコードすると、数値的な確率計算 [19] を伴うことを表す。ここで、m はクロック変数かコスト計算とになる。

に用いる電力消費を表す変数とした。

2間に制限を与えた範囲で最大値を超えないことを議

y.

u.(IL ⇒mv. (LS ∧ (y≤x + 10)∧(v≤u + 50)))

この式 φ1 は、時区間とコスト計算区間が同一である。しかし、Deep Sleep から High Power までの条
件 φ2 を同時に考えてみよう。

2

τ

F

使用していると、いつかは最大値を超える。使用時

τx.(DS ⇒ 3

τF

電力消費量は使用時間に比例することから、連続

m

x.

3

力が与えられた最大値 Max を超えないこと」といった性質がある。

τFから状態 Light Sleep(LS と略す) までに消費した電10 で消費電力量が 50 を超えないとした。
Fして考える。例えば、「状態 Idle Listen(IL と略す)のような論理式 φ1 で表現することができる。時区間

F

次に、PCA に対して調べる検査性質を図 2 を参照

このような凍結限量子を用いると、冒頭の例は次F

2. 2. 3 検査性質

y.(HP ∧ (y≤x + 100)))

論すべきである。つまり、ある条件を満たす状態を以上の 2 つの条件が両方とも成り立つことは、φ1 ∧ φ2

開始時点とし、もうひとつの条件を満たす状態を終と表すことができる。このように制約条件を柔軟に表了時点とする。そのような有界な時区間の範囲内で、現したい。連続量に関わる性質を表現した論理体系を別途決められた処理の消費電力量（一般にコストと導入し、電力消費オートマトンに対するモデル検査の呼ぶ）について、与えられた制約条件を満たすか否

方法が必要になる。以降、電力消費オートマトンならかを検査する。これを有界な時区間でのコスト制約

びに検査性質を表現する時相論理体系を厳密に導入（duration-bounded cost constraints）の問題と呼ぶ。

し、より詳細にモデル検査の問題を考える。

時間オートマトンに対する性質として、有界な時区間での到達性解析 (duration-bounded reachability)の方法が決定可能であることが知られている [2]。これは、有界な時区間内で、その区間の開始状態から終3 電力消費の振る舞い仕様
電力消費オートマトンを重み付き時間オートマト
ン [5] [6] として表す。

了状態までのコストが、与えられた制約を満たすような経路が存在することを確認する。時区間とコスト計

3. 1 電力消費オートマトン

算区間が同一である時の到達性解析である。本稿で取電力消費オートマトン (Power Consumption Au-

り扱う問題は、これよりも広い条件を検査することにtomaton, PCA と略記) A は、アトミックな命題の有なる。

限集合 P rop に対して、次のように定義される。

上記の例に示した PCA の振る舞いに関わる仕様

(ν×e)(x) = ν(x)×e⟨ Loc, C, D, Σ∪{ϵ}, Edg, F low, Inv, Lab ⟩以下、構成要素を説明する。

今、2 つの PCA A1 、A2 を考えて、変数について

1. Loc は、ロケーションの有限集合。

(C1 ∪D1 )∩(C2 ∪D2 ) = ∅ とする。これら 2 つの PCA

2. C はクロック変数の集合、 D は重み変数の集合。

の並行合成 A1 ||A2 を同期積として定義する。A1 がC と D は互いに素であり、C∩D = ∅。クロック変数 x、自然数 n、オペレータ ◃▹ ∈ {<, ≤, =, ≥, >}に対して、x ◃▹ n、x1 − x2 ◃▹ n、の形をした制
約式の集合をクロック制約 Z(C) と呼ぶ。

3. Σ は、入力記号の有限集合であり、 ϵ は記号が空の場合を示す。

同期アルファベット a∈(Σ1 ∩Σ2 ) で離散遷移する時、A2 も離散遷移する。
最後に、電力消費オートマトン A は、必要に応じて、内部変数 V を持つ重み付き拡張時間オートマト
ン (Extended Weighted Timed Automaton) ⟨A, V ⟩とする。

4. Edg は遷移を表し、Loc×Z(C)×Σ×2C ×Loc
g,a,rの部分集合。要素 (l1 , g, a, r, l2 ) を、l1 −→ l2 の

3. 2 動作意味

ように表記する。ここで、g はクロック制約から

PCA A の動作意味をラベル付き遷移システム

なるガード条件、a は入力記号、r はリセットす（Labeled Transition System、LTS と略記) で与えるクロック変数の集合を示す。

る。LTS ⟨ S, T ⟩ を以下のように構成する。

Edge のすべての要素に対して、ある遷移元か

状態空間 S は、ロケーション l、クロック変数のバ

らの遷移が、真となるガード条件と入力記号をリュエーション v と重み付き変数のバリュエーション

決めた時、その遷移先が唯一に決定できる場合、w の組を状態とする集合である。

決定性 PCA (deterministic PCA) と呼ぶ。

5. F low は、各ロケーションにおける重みの変化を表すダイナミックス。R+ を非負の実数、RD+ =D
D→R+ として、F low : Loc→(RD+ →R+ ) となる。

ロケーションに与えられたクロック制約は常に満たされる。
状態 遷移 T は、通常 遷移と 滞留遷 移から なり、
d,e

d,ϵ

T = { −→ } ∪{ −→ } である。詳細を以下に示す。

PCA は各ロケーション (ℓ) での単位時間あたℓ

りの電力消費が一定 (M ) なので、重みのバリュ
エーションを w、消費電力量を表す変数を p とℓ

すると、F low(ℓ)(w)(p) = dp/dt = M となる。

6. Inv は、各ロケーションに付されたクロック制
約。Inv : Loc→Z(C)7. Lab は、各ロケーションで成り立つアトミックな命題の集合。Lab : Loc→2P rop
上記で、クロック変数と重み変数に対するバリュエー
ション ν : RC∪Dを用いた。リセット、遅延、乗算+を次のように定義する。
{
0
ν[r](x) =ν(x)D{(l, v, w) ∈ Loc × RC
+ × R+ | v |= Inv(l) }if x∈rotherwisee• 離散遷移 (l1 , v1 , w)−→(l2 , v2 , w)g,a,r∃(l1 −→ l2 ) ∈ Edg, v1 |=g, v2 = v1 [r]d• 時間遷移 (l, v, w1 )−→(l, v + d, w2 )d ∈ R+ , w1 = f (0), w2 = f (d),∀t ∈ ]0, d[ |v + t |=Inv(l) ∧ df /dt = F low(l)遅延 d だけの時間が経過し (v + d)、同時に、重み変数も更新される。上記では、一般形として、開区間 ]0, d[ で微分可能な時間の関数 f を用いて表現した。個別の重み変数 p について考えると、ロケーション ℓ で dp/dt = M ℓ であり、

w2 (p) = M ℓ ×d + w1 (p) となる。
ϵ

• 空遷移 (l1 , v1 , w)−→(l2 , v2 , w)g,ϵ,r∃(l1 −→ l2 ) ∈ Edg, v1 |=g ∧ F low(l) = ∅(ν + d)(x) = ν(x) + d

入力アルファベットが ϵ で重みが不変となるよう

ない ϕ を閉じた論理式と呼ぶ。また、コスト制約式

な離散遷移。
d,eは、π1 <π2 ≡¬(π2 ≤π1 )、π1 =π2 ≡(π1 ≤π2 )∧(π2 ≤π1 )dなので、制約式の集合 Z(C∪D) である。さらに、標• 通常遷移 (l1 , v1 , w1 )−→(l2 , v2 , w2 )時間遷移 (l1 , v1 , w1 )−→(l1 , v, w2 ) の後に、離散e

準的な略記を導入する。特に、3ϕ≡trueUϕ（Even-

遷移 (l1 , v, w2 )−→(l2 , v2 , w2 ) が生じる。
d,ϵtually オペレータ）、2ϕ≡¬(3¬ϕ)(Globally オペレー

dタ)、ϕ1 Rϕ2 ≡¬(¬ϕ1 U¬ϕ2 ) (Release オペレータ) で• 滞留遷移 (l, v1 , w1 )−→(l, v2 , w2 )時間遷移 (l, v1 , w1 )−→(l, v, w2 ) の後に、空遷移
ϵ(l, v, w2 )−→(l, v2 , w2 ) が生じる。

ある。

d,e

この時、遷移列を、通常遷移 −→ からなる有限列で

4. 2 fWLTL の意味

あるか、あるいはそのような有限列の後に、0 個以上

時点表示の考え方で、fWLTL 式の意味定義を与え

d,ϵの滞留遷移 −→ からなる無限列であると定義する。
なお、滞留遷移が定義されているロケーションを受理• 時間付き状態列ρ = ρ0 ρ1 · · ·。た だ し 、状 態 σ j = (lj , vj , wj ) と 時 点 τ j に 対 し て 、状態と考える。
さらに、PCA A の受理列 L(A) を時間付き状態列

ρ の全体とする。時点 τ j ∈R+ の列が時間の経過を表dし、τ = 0、時間遷移 −→ に対して τ
0る。その準備として、いくつかの記号を導入する。

i+1i= τ +dとする。状態 σ ∈S に対して、ρ = (σ , τ ) として、
j

j

j

j

ρ = ρ ρ · · · である。このように構成した ρ に対し
0 1て、ρ∈L(A) である。

ρj =(σ j , τ j )= (lj , vj , wj , τ j ) は時間付き状態。
• 変数の可算無限集合 V ar
• 凍結限量子で束縛された変数の解釈
Γ : V ar → R+
• Γ[x := e] は変数 x に e (e∈R+ ) を割当て、x 以
外は不変
組み ⟨ ρ, Γ ⟩ が、 fWLTL 式 ϕ を満たすことは、時4 検査性質の表現形式

点表示によって、以下のように帰納的に定義された充PCA が表す電力消費振る舞いに対する検査性質の

足関係 |= に対して、⟨ ρ, Γ ⟩ |= ϕ となることである。

⟨ ρj , Γ ⟩ |= ciﬀ

c ∈ R+⟨ ρj , Γ ⟩ |= x + c

iﬀ

Γ(x) + c ∈ R+

4. 1 fWLTL の構文⟨ ρj , Γ ⟩ |= piﬀ

p ∈ Lab(lj )凍結限量子を持つ重み線型時相論理 (Weighted Lin-⟨ ρ , Γ ⟩ |= π1 ≤ π2

iﬀ

Γ(π1 )≤Γ(π2 )ear Temporal Logic with freeze quantiﬁers、fWLTL⟨ ρ , Γ ⟩ |= ¬ϕiﬀ⟨ ρj , Γ ⟩ ̸|= ϕと略記）の構文を示す。

⟨ ρj , Γ ⟩ |= ϕ1 ∧ ϕ2

表現方法を述べる。

:= c

定数 ∈ N|x + c

加算演算:= p

アトミックな命題 ∈ P rop

iﬀ| π1 ≤ π2

大小比較演算and ⟨ ρi , Γ ⟩ |= ϕ1 for all i (j≤i<k)

| ¬ϕ

論理否定

| ϕ1 ∧ ϕ2

論理積iﬀ⟨ ρj , Γ ⟩ |= ϕ1 , and ⟨ ρj , Γ ⟩ |= ϕ2⟨ ρj , Γ ⟩ |= ϕ1 U ϕ2
⟨ ρk , Γ ⟩ |= ϕ2 for some k ≥ j,

⟨ ρj , Γ ⟩ |=iﬀ

Until 演算子

⟨ ρ , Γ ⟩ |=|F

x . ϕx

凍結限量子

iﬀ

|

τ

x . ϕx

凍結限量子（時点）mx . ϕx⟨ ρj , Γ[x := (v j ∪wj )(m)] ⟩ |= ϕx| ϕ1 U ϕ2

j

m

τ

F

F

ϕ

j

F

π

j

x . ϕx⟨ ρj , Γ[x := τ j ] ⟩ |= ϕx

5 モデル検査
ここで、アトミックな命題 p ∈ P rop、変数 x ∈ V ar

電力消費オートマトン A が生成する遷移列の全体は論理式 ϕx において自由出現する。自由変数を持たを L(A) とする時、A に対する閉じた fWLTL 式 ϕのモデル検査 A, Γ |= ϕ は、全ての時間付き状態列

ることであり、先に述べた Real-time Maude の方法ρ∈L(A) と空の Γ に対して、⟨ ρ , Γ ⟩ |= ϕ が成り立で σ(R) を生成すれば良い。ただし、決定性 PCA につかを調べることである。

対象を限定する。

0

PCA は、Weighted Timed Automaton(WTA) [5]あるいは Linear Priced Timed Automaton(LPTA)

6 関連研究[6] であるが、遷移エッジ (Edg) に重みを持たない、

本稿では、アンドロイド・アプリケーションの電力

つまり、状態にのみ重みが定義されている点が異な消費問題を対象として、振る舞い記述として PCA、る。WTA と LPTA は時間オートマトン (TA) の拡

性質表現として fWLTL を提案し、モデル検査の方法

張である。TA の Metric Temporal Logic (MTL) にについて考察した。以下、振る舞い記述と性質表現の対するモデル検査は決定不能で、MTL のサブセット

両方について関連研究と比較する。

に制限しなければならない [16]。WTA の MTL に対するモデル検査は決定不能である。

PCA は線型ハイブリッドオートマトン (LHA) [4]であり、ストップウォッチ・クロック変数を持つ n レー

凍結限量子を持つ時相論理として TPTL [3] があト時間システム (n-RTS) で表現できる [11]。電力消る。TPTL は、TA が生成する時間付き文字列に対し費は観測変数で表現できるので、これを重みとすれて定義されており、束縛変数は時点 (その値 now) をば、重み付き時間オートマトン (WTA) [5] あるいは「凍結」する。TPTL は、MTL をサブセットに含み。

プライス付き時間オートマトン (LPTA) [6] と見なす

TA に対するモデル検査は決定不能であるが、離散時こともできる。ただし、PCA では重みは状態にのみ

間 (N ) に制限すれば決定可能である。

定義されており、遷移エッジは重みを持たない。性質

以上から、PCA の fWLTL に対するモデル検査は検証の基本となる到達性解析については、nRTS は決決定不能と考えられる。そこで、本稿では、Real-time

定不能であるが、WTA と LPTA は等価であり、時Maude [15] の時間有界探索とサンプリング抽象の方

間オートマトン (TA) の方法に帰着できるので、決定法を採用する。明示的に時間進行を取り扱う体系に基可能である。

づく。有限長の時間付き状態列 ρ̂ を対象として、与えTA に 対 し て 、有 界 な 時 区 間 で の 到 達 性 解 析

られた A が状態変化を引き起こすインデックス j を(duration-bounded reachability) [2] がある。文献 [5]カバーするように論理式を検査するサンプリング点[6] は、この問題を拡張して、重み（プライス）を尺を選ぶ有界モデル検査法である。一般には、オーバー

度とする最適経路や最小経路を含む到達性解析の方

サンプリングとなる。ひとつの方法として、PCA な法を示した。fWLTL は、有界な時区間での到達性は

らびに fWLTL 式を、Real-time Maude に変換すれ表現することが可能であるが、最適経路等の評価関数

ば良い。文献 [14] は、PCA を n-RTS として変換するが必要な問題を扱うことはできない。より柔軟な性質

方法の概略を述べている。この方法を参考にすれば表現を重視し、時相論理を採用した。

よい。

fWLTL の凍結限量子は、これを最初に導入した

PCA の重みが確率コンポーネントを持つ場合、統TPTL [3] を参考にした。TPTL は、TA が生成する

計モデル検査の方法 [19] を用いる。確率変数 R に依

時間付き文字列に対して定義されており、束縛変数は存して生成される遷移列 σ(R)∈L(A(R)) と fWLTL

時間点 (now) を「凍結」する。一方、fWLTL は、重式 ϕ に対して、B(R)≡(σ(R), Γ|=ϕ) とする。充足す

みによって表現した電力消費値も参照できるように拡る時に B = 1、充足しない時に B = 0 とすると、B張した。TPTL の凍結限量子 x.ϕx は、fWLTL では、
τx.ϕx と表現する。時間以外の連続変数にも拡張すが 1 となる確率は p のベルヌーイ分布となる。統計

F

モデル検査は、試行を繰り返すことで、生起確率 p をる凍結限量子は文献 [10] の ↓x=m ϕx がある。fWLTL

統計的に得る方法で、検査性質 ϕ が成り立つ確率をのF求めることができる。試行とは、σ(R), Γ|=ϕ を調べ

mx.ϕx に相当する。

文献 [9] は LPTA を対象として、時間遷移の遅延時

間値に確率分布を導入した動作意味を定義し、統計モデル検査を適用する。遷移エッジが持つクロック・
ガード条件を持つとき、遅延を非決定的に選択する通常の LPTA と異なり、条件を満たす遅延が確率的に与えられる。なお、TA のモデル検査が時間制約の記号的な表現を採用しているのに対して、文献 [8] [9] は
時間進行を明示的に取り扱うことで、統計モデル検査を実現した。PCA の確率コンポーネントは重みに与えられている点が異なるが、Real-time Maude が時間進行を明示的に扱うので統計モデル検査が可能になる。

7 おわりにモデルベース解析の提案 [11] [12]、DVFS の影響に対する考察 [13]、Real-time Maude を用いる予備検討[14] を踏まえて、本稿では、検査性質の表現とモデル検査の観点から、電力消費オートマトンを再検討した。関連研究を調べると、モデル検査は決定不能になることがわかる。したがって、近似を導入する方法や統計的モデル検査が適切であることを論じた。今後、

Real-time Maude への変換による自動解析の方法を詳細に検討する。

謝辞 口頭発表 [11] に対して、電力消費オートマト
ンとプライス付き時間オートマトンの関連性を指摘して下さった名古屋大学大学院の結縁祥治教授に感謝する。また、本研究の一部は科学研究費助成事業課題
番号 26330095 の助成を得て実施した。
参 考 文 献[ 1 ] Android. http://developer.android.com.
[ 2 ] R. Alur, C. Courcoubetis, and T.A. Henzinger.
Computing Accumulated Delays in Real-Time System, In Proc. CAV 1993, pp.181-193, 1993.
[ 3 ] R. Alur and T.A. Henzinger. A Really Temporal Logic, J. Accoc. Comp. Machin., Vol.41, No. 1,
pp.181-204, 1994.
[ 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 ofHybrid Systems, Theor, Comp. Sci., No.138, pp.324, 1995.

[ 5 ] R. Alur, S. La Torre, and G.J. Pappas. Optimal Paths in Weighted Timed Automata, In Proc.
HSCC 2001, pp.49-62, 2001.
[ 6 ] G. Behrmann, A. Fehnker, T. Hune, K. Larsen,
P. Pettersson, J. Romjin, and F. Vaandrager.
Minimum-Cost Reachability for Priced Timed Automata, In Proc. HSCC 2001, pp.147-161, 2001.
[ 7 ] P. Bouyer, U. Fahrenberg, K.G. Larsen, and N.
Markey. Timed Automata with Observers under Energy Constraints, Proc. HSCC 2010, 2010.
[ 8 ] P. Bulychev, A. David, K.G. Larsen, A. Legay,
G. Li, D.B. Poulsen, and A. Stainer. Monitor-Based
Statistical Model Checking for Weighted MetricTemporal Logic, In LPAR-18, pp.168-182, 2012.
[ 9 ] A. David, K.G. Larsen, A. Legay, M. Mikucionis,
D.B. Poulsen, J. van Vliet, and Z. Wang. Statistical Model Checking for Networks of Priced Timed
Automata, In Proc. 9th FORMATS, pp.80-96, 2011.
[10] S. Demri, R. Lazic, and D. Nowak. On the Freeze
Quantifier in Constraint LTL : Decidability andComplexity, Information and Computation, 205(1),pp.2-24, 2007.
[11] 中島震. スマートフォン・アプリ電力消費のモデル
ベース解析, 情報処理学会組込みシステム研究会, 2013.
[12] S. Nakajima. Model-based Power Consumption
Analysis of Smartphone Applications, In Proc.
ACES-MB 2013, 2013.
[13]
中島震. 省電力プロセッサのアンドロイド・アプリ
電力消費モデルへの影響, 電子情報通信学会ソフトウェ
アサイエンス研究会, 2014.
[14] S. Nakajima. Everlasting Challenges with the
OBJ Language Family, In Proc. SAS 2014, pp.478493, 2014.
[15] P.C. Olveczky and J. Meseguer. Semantics andPragmatics of Real-Time Maude, Higher-Order andSymbolic Computation, vol.20, no.1-2, pp.161-196,
2007.
[16] J. Ouaknine and J. Worrell. Some Recent Results in Metric Temporal Logic, In Proc. FORMATS
2008, pp.1-13, 2008.
[17] 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, 2011.
[18] A. Pathak, Y.C. Hu, and M. Zhang. Where is theenergy spent inside my app?: Fine Grained Energy
Accoutning on Smartphones with Eprof, In Proc.
EuroSys’12, 2012.
[19] H.L.S. Younes, M. Kwiatkowska, G. Norman,
and D. Parker. Numerical vs. Statistical Probablistic Model Checking, J. STTT, 8(3), pp.216-228,
2006.
[20] L. Zhang, M.S. Gordon, R.P. Dick, Z.M. Mao, P.
Dinda, and L. Yang. ADEL : An Automatic Detector of Engery Leaks for Smartphone Applications,
In Proc. CODES+ISSS’12, 2012.