| 研究課題/領域番号 |
26330095
|
|---|
| 研究機関 | 国立情報学研究所 |
|---|
研究代表者 |
中島 震 国立情報学研究所, アーキテクチャ科学研究系, 教授 (60350211)
|
|---|
| 研究期間 (年度) |
2014-04-01 – 2017-03-31
|
| キーワード | モデルベース開発 / 機能外要求 / 電力消費 / モデル検査 / ハイブリッドシステム |
|---|
| 研究実績の概要 |
電池容量の小さいスマートフォンやタブレット等では、アプリケーションプログラムの実行が消費電力に与える影響が大きな問題となる。機能振る舞いが意図通りであっても、電池消耗が予想外に大きくなることがある。このような「電力バグ」を、ソフトウェア開発の早期に発見し除去する方法を確立する必要がある。
本研究課題では、機能振る舞い仕様に電力消費に関わる性質を追加した形式モデル「電力消費オートマトン (PCA)」を新たに考案し、プログラム（アプリケーションおよび基盤ソフトウェア）ならびにハードウェアコンポーネントの振る舞いをPCAで表現する方法を確立した。この時、電力消費に関わる性質に関する解析法をPCAに対するロジック・モデル検査の問題に帰着できる。特に、アンドロイド・スマートフォンのWiFi利用アプリを具体的な例題として、提案方式によって、電力バグの発見が可能なことを示した。また、電力バグがあると判明した検査対象に対して、当該バグの原因箇所を自動発見する方法を考案し、実験によって原因箇所が特定できることを確認した。
モデル検査に基づく電力消費解析の方法は、形式手法分野のトップ国際会議FM2015で採択された。また、平成２６年度の情処学会研究会発表に対して山下研究賞を受賞した。これらから、本研究課題の成果が、国内外で高い評価を得ていることがわかる。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
電力消費に関わる解析問題をロジックモデル検査に帰着できることを示し、アンドロイド・スマホの具体的な例によって有効性を確認した。さらに、欠陥箇所を自動発見する方法を考案した。形式手法分野のトップ国際会議FM2015で採択される等、国際的な評価を得ている。
|
| 今後の研究の推進方策 |
電力消費解析ならびに電力バグ欠陥箇所の自動特定の方法を取り扱う研究は他にはなく、本研究課題ではじめて全体像を提示したものである。問題ならびに解法についての形式化を系統的に行うことで、理論面での整理を行い、論文にまとめる。
|
| 次年度使用額が生じた理由 |
次年度に海外との研究交流等によって本助成金を重点的に使用することを計画し、今年度は本助成金の使用計画を変更し、基盤研究費によって研究活動に必要な予算執行を行った。
|
| 次年度使用額の使用計画 |
海外研究者（フランス・ツールーズ等）との研究交流ならびに形式手法分野の国際会議参加の目的で、本助成金を使用する。
|
