2014 Fiscal Year Research-status Report
スマートフォン・アプリケーション電力消費のモデルベース解析に関する研究
| Project/Area Number |
26330095
|
|---|
| Research Institution | National Institute of Informatics |
|---|
Principal Investigator |
中島 震 国立情報学研究所, アーキテクチャ科学研究系, 教授 (60350211)
|
|---|
| Project Period (FY) |
2014-04-01 – 2017-03-31
|
| Keywords | モデルベース開発 / 機能外要求 / 電力消費 / モデル検査 / ハイブリッドシステム |
|---|
| Outline of Annual Research Achievements |
電池容量の小さいスマートフォン等では、アプリケーションプログラム実行に起因する消費電力が大きな問題となる。機能振舞いが意図通りであっても、予想外の電池消耗を引き起こす「電力バグ」が混入することがあり、このようなバグを開発の早期段階で発見し除去する方法を確立する必要がある。
本研究課題では、アプリケーションに起因する電力消費の形式モデルを表す「電力消費オートマトン（PCA）」を考案した。これは、従来、重み付き時間オートマトンと呼ばれていた体系に相当する。この時、電力消費に関わる不具合を検査する性質は、与えられた指定時区間における電力消費の解析問題となる。本研究課題では、これを「有界時区間におけるコスト制約問題」として整理した。次に、このような性質を具体的に表現する方法として、「凍結限量子を持つ線形時間論理（fWLTL）」を提案した。この時、「有界時区間におけるコスト制約問題」は、fWLTL論理式のPCAに対するロジックモデル検査の問題に帰着できる。一方、このロジックモデル検査は一般には決定不能であることから、近似的な方法を考案して自動検査を可能にする必要がある。凍結限量子の位置を制限すること、検査式の形を限定すること、によって、Real-Time Maudeを用いた自動検査が可能になることを示した。WiFi無線を使う例題を用いて、提案方式によって、確かに電力消費に関わる性質検査が自動化可能なことを確認した。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
電力消費に関わる問題が、自動検証の代表的な方法であるロジックモデル検査に帰着できることを、具体例を用いて示した。国内外の研究会等での発表によって、この方法が真にオリジナルであることを確認した。実際、電力消費の問題を形式検証技術の枠組みで解決する試みは他には見当たらず、本研究課題が、最も進んでいる。
|
| Strategy for Future Research Activity |
アンドロイド・フレームワーク上で作動するアプリケーション・プログラム（いわゆるアプリ）の特徴を取り込んだ形式モデル（Activityモデル）を表現可能なように、PCAを拡張する。画面遷移を有する典型的なアプリを例題として、この拡張PCAに対する電力消費問題の詳細的な解決法についての研究を進める。
|
| Causes of Carryover |
次年度に海外での国際学会発表によって本助成金を重点的に使用することを計画し、今年度は本助成金の使用計画を変更し、基盤研究費によって研究活動に必要な予算執行を行った。
|
| Expenditure Plan for Carryover Budget |
形式手法のトップレベル国際会議FM2015（６月オスロ・ノルウェーで開催）での論文発表を含めて、主として、複数回の海外での研究成果発表を行う目的で、本助成金を使用する。
|
