| Project/Area Number |
15700015
|
|---|
| Research Category |
Grant-in-Aid for Young Scientists (B)
|
| Allocation Type | Single-year Grants |
|---|
| Research Field |
Fundamental theory of informatics
|
|---|
| Research Institution | Nara Institute of Science and Technology |
|---|
Principal Investigator |
新田 直也 奈良先端科学技術大学院大学, 情報科学研究科, 助手 (20346307)
|
|---|
| Project Period (FY) |
2003 – 2004
|
| Project Status |
Completed (Fiscal Year 2004)
|
| 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)
|
|---|
| Keywords | モデル検査 / 項書換え系 / 無限状態システム / プッシュダウンシステム / 例外処理 / グラフ書換え系 |
|---|
| Research Abstract |
本研究では,計算機システムの自動検証技術の1つであるモデル検査法と項書換え系の理論を融合し,一般に無限の状態空間を持つソフトウェアに対しても自動検証できるようモデル検査法を拡張することを目指した.特に本年度は,以下の2点を中心に研究を進めた.
●モデル検査可能なクラスの拡張
昨年度の研究において研究代表者らは,拡張PDS(LL-GG-TRS)と呼ばれるTRSの部分クラスを定義し,そのLTLモデル検査アルゴリズムを開発した.さらに,拡張PDSを用いることにより,従来検証が困難であった例外処理機能(exception handling)付き再帰プログラムが検証可能となることも発見した.本年度は実用性のさらなる向上を目指し,オブジェクト指向型プログラムをも検証できるよう,新しい計算モデルAliasingPDSをグラフ書換え系の部分クラスとして定義し,そのモデル検査アルゴリズムを開発した.AliasingPDSは,再帰呼び出しとオブジェクトの無制限な動的生成を同時に扱いつつ,到達可能性判定問題が決定可能となるよう設計された実用的かつ強力な計算モデルである.AliasingPDSの上にJavaプログラムをモデル化することで,より現実的なソフトウェアモデル検査法構築の基盤となることが期待される.
●モデル検査システムの開発
モデル検査システムの木言語処理部(所属判定,積集合演算)に関する基本調査および設計を行った.
|
Report
(2 results)
Research Products
(5 results)
