| 研究概要 |
信頼性の高い情報システムを実現するためには,設計上の誤りを開発のできるだけ早期の段階で検出することが非常に重要となる.そのための手法として,システム上で起こりうる状態を網羅的に調べるモデル検査と呼ばれる方法がある.特に,状態集合や遷移関係を論理関数によって表現することで効率良く検査を行う方法は記号モデル検査と呼ばれ,ハードウェアシステムの検証に広く利用されている.しかしながら,現在の段階ではソフトウェアに対するモデル検査手法は十分に確立されていると言いがたい.
そこで本研究では,ソフトウェアのための新しい記号モデル検査手法を考案し,その方法を実装した解析システムの開発を行った.より具体的には,限定モデル検査(Bounded Model Checking)と呼ばれる新しい記号モデル検査手法の利用を試みた.この手法は,探索する状態系列の長さを予め限定することで,少なくとも処理の早い段階で現れる誤りを検出するという方法である.
これまでの研究で,時相論理の良く知られたクラスである線形時間論理に属する論理式を検証するアルゴリズムが示されていたが,実際に開発されている検証系はその中の極一部の論理式にしか対応していなかった.そこでこのアルゴリズムを完全な形で実装した検証系の開発を行った.
この過程で,検証対象となる並行システムがinterleavingなセマンティクスを持つ場合,このアルゴリズムでは効率の良い検証が困難であることが分かった.そこで,論理関数の新たな構成法を開発し,ペトリネットや,通信電話サービス等の上記の性質を有するシステムの検証に適用した.その結果,特にシステムの状態数が大きくなった場合,提案法が記号的な手法を用いない従来のモデル検査手法に比較して,非常に効率の良い検証が可能であることを示すことができた.
|
