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