電力消費はバッテリー駆動システムにおける代表的な機能外要求に関係する。バッテリー容量は小さいことから、長期間の作動を実現するには、電力消費を低減する必要がある。電力を消費する実体はハードウェア部品であるが、その部品を利用するアプリケーション・プログラムに不具合があると、予期しない量の電力が消費されてしまう。このような電力バグは、プログラム設計の欠陥に起因するので、開発上流工程で早期に除去したい。本研究課題は、電力消費のモデルベース解析の方法を検討する。重み付き時間オートマトンをベースとする形式モデルを用いることで、電力消費解析をロジック・モデル検査の問題に帰着できることがわかった。
|