2003 Fiscal Year Annual Research Report
| Project/Area Number |
15700015
|
|---|
| Research Institution | Nara Institute of Science and Technology |
|---|
Principal Investigator |
新田 直也 奈良先端科学技術大学院大学, 情報科学研究科, 助手 (20346307)
|
|---|
| Keywords | モデル検査 / 項書換え系 / 無限状態システム / プッシュダウンシステム / 例外処理 |
|---|
| Research Abstract |
本研究では,計算機システムの自動検証技術の1つであるモデル検査法と項書換え系の理論を融合し,一般に無限の状態空間を持つソフトウェアに対しても自動検証できるようモデル検査法を拡張することを目指している.本年度は,この目標にしたがって主に基礎理論の構築を行ってきた.その結果,当初の予想通り項書換え系に以下のような制限を加えたクラスに対して,線形時相論理式(LTL式)によるモデル検査問題が決定可能となることを証明することができた.
(1)書換え位置をルートに限定する.
(2)書換え規則を左線形(規則左辺に同じ変数が2回以上出現しない)とする.
(3)書換え規則の左辺と右辺における変数の出現位置に一定の制約を加える.
これらの制限を加えても,再帰プログラムのモデルとして広く用いられているプッシュダウンシステムをシミュレートするのに十分であることは,当初の予想通りであったが,それに加えて,(a)本クラスはプッシュダウンシステムのクラスより真に広いこと,(b)例外処理を含む再帰プログラムが真に広いことを示す一例になっていること,を示すことができた.特に(b)は,本研究の有用性を示す重要な発見であると考える.
また,本研究の情報セキュリティ,特に暗号プロトコルの安全性検証への応用について理論的検討を重ねている.
なお,本研究に関して,2003年7月に研究代表者は「社団法人情報処理学会 平成15年度山下記念研究賞」を受賞している.
|
Research Products
(3 results)
-
[Publications] Naoya Nitta, Hiroyuki Seki: "An extension of pushdown system and its model checking method"Technical Report NAIST-IS-TR2003007, Nara Institute of Science and Technology. (ウェブで公開). (2003)
-
[Publications] Naoya Nitta, Hiroyuki Seki: "An extension of pushdown system and its model checking method"Proceedings of the 14^<th> International Conference on Concurrency Theory (CONCUR2003), LNCS 2761. 281-295 (2003)
-
[Publications] 新田 直也: "Aliasing-PDS : オブジェクト指向プログラムのモデル検査のための新しい計算モデル"シンポジウム「システム検証の科学技術」予稿集. 37-46 (2004)
