| Budget Amount *help |
¥2,500,000 (Direct Cost: ¥2,500,000)
Fiscal Year 2004: ¥1,300,000 (Direct Cost: ¥1,300,000)
Fiscal Year 2003: ¥1,200,000 (Direct Cost: ¥1,200,000)
|
|---|
| Research Abstract |
本研究では,計算機システムの自動検証技術の1つであるモデル検査法と項書換え系の理論を融合し,一般に無限の状態空間を持つソフトウェアに対しても自動検証できるようモデル検査法を拡張することを目指した.特に本年度は,以下の2点を中心に研究を進めた.
●モデル検査可能なクラスの拡張
昨年度の研究において研究代表者らは,拡張PDS(LL-GG-TRS)と呼ばれるTRSの部分クラスを定義し,そのLTLモデル検査アルゴリズムを開発した.さらに,拡張PDSを用いることにより,従来検証が困難であった例外処理機能(exception handling)付き再帰プログラムが検証可能となることも発見した.本年度は実用性のさらなる向上を目指し,オブジェクト指向型プログラムをも検証できるよう,新しい計算モデルAliasingPDSをグラフ書換え系の部分クラスとして定義し,そのモデル検査アルゴリズムを開発した.AliasingPDSは,再帰呼び出しとオブジェクトの無制限な動的生成を同時に扱いつつ,到達可能性判定問題が決定可能となるよう設計された実用的かつ強力な計算モデルである.AliasingPDSの上にJavaプログラムをモデル化することで,より現実的なソフトウェアモデル検査法構築の基盤となることが期待される.
●モデル検査システムの開発
モデル検査システムの木言語処理部(所属判定,積集合演算)に関する基本調査および設計を行った.
|
