| 研究概要 |
信頼性の高い情報システムを実現するためには,設計誤りを開発のできるだけ早期の段階で検出することが非常に重要となる.そのための手法として,システム上で起こりうる状態を網羅的に調べるモデル検査と呼ばれる方法が知られている.本課題では,近年になって開発されたモデル検査手法である限定モデル検査(Bounded Model Checking)を,非同期的な並行動作を有するソフトウェアシステムに適用するための研究を行った.
限定モデル検査では,遷移関係を表現した論理関数からシステムの誤った振舞いを表現する一つの論理式を構成する.この論理式が充足可能であればシステムに設計誤りがあることを結論できる.しかし,従来の手法では,ソフトウェアシステムを対象とした場合,この論理式が非常に大きくなってしまい,効率良く検証が行えなかった.
本研究では,平成13年度に開発した新しい論理式構成手法を改良し,1)これまで扱うことのできなかった種類の誤りの検出,及び,2)検証効率の向上,を実現した.
1については,これまで安全性に関する誤りのみ検出可能であったものを,活性に関する性質についても可能にした.2については,論理式の生成前にシステムの動作規則の依存関係を予め考慮するような前処理を行うことで実現した.
ペトリネットと通信電話サービスを具体的な検査対象として,これらの提案手法を実装した.実験の結果,従来の限定モデル検査や,他のモデル検査手法に比べ,非常に効率の良く設計誤りが検出できることが分かった.
|
