|
電池容量が小さなスマートフォンやタブレット等では、アプリケーション・プログラムの実行が消費電力に与える影響が大きな問題となる。プログラムの機能振る舞いが意図通りであっても、電池消耗が予想外に大きくなることは好ましくない。このような「電力バグ」を、ソフトウェア開発の早い段階で発見し除去する方法を確立する必要がある。
電力バグは新しい問題であることから、本研究課題では、アンドロイド・スマートフォンを対象として、電力消費の傾向を実験計測によって確認、さらに、電力消費の問題を系統的に取り扱うことを目的とした形式モデルの提案、という２つの観点で研究を進めた。
機能振る舞い仕様と電力消費に関わる性質を一つの枠組みで表現する形式モデル「電力消費オートマトン（PCA）」を新たに考案し、ソフトウェア（アプリケーションならびに基盤ソフトウェア）ならびにハードウェア部品の振る舞いをPCAで表現する方法を確立した。さらに、電力消費に関わる性質を拡張版時相論理式として表現することで、電力消費の分析を、自動検証の方法であるモデル検査問題に帰着させた。アンドロイド・スマートフォンを具体例として、本提案方式によって、電力バグの自動発見が可能なtことを示した。さらに、PCAならびに検査式の双方を、有界モデル検査と同様な方法で論理式で書き表すことで、バグ箇所の自動発見が可能なことを示した。
期間内に行った国際学会での発表５件の内容を中心として、研究成果の全体像を系統的にまとめた論文を執筆した。この論文を寄稿した学術専門書が公刊された。
|
