項書換え系を対象としたモデル検査手法に関する研究
項書換え系を対象としたモデル検査手法に関する研究
术语重写系统模型检验方法研究
批准号：
15700015
负责人：
新田 直也
金额：
$1.6万
依托单位国家：
日本
项目类别：
Grant-in-Aid for Young Scientists (B)
财政年份：
2003
资助国家：
日本
项目状态：
已结题
起止时间：
2003 至 2004
中文摘要
翻译
本研究では,計算機システムの自動検証技術の1つであるモデル検査法と項書換え系の理論を融合し,一般に無限の状態空間を持つソフトウェアに対しても自動検証できるようモデル検査法を拡張することを目指した.特に本年度は,以下の2点を中心に研究を進めた.●モデル検査可能なクラスの拡張昨年度の研究において研究代表者らは,拡張PDS(LL-GG-TRS)と呼ばれるTRSの部分クラスを定義し,そのLTLモデル検査アルゴリズムを開発した.さらに,拡張PDSを用いることにより,従来検証が困難であった例外処理機能(exception handling)付き再帰プログラムが検証可能となることも発見した.本年度は実用性のさらなる向上を目指し,オブジェクト指向型プログラムをも検証できるよう,新しい計算モデルAliasingPDSをグラフ書換え系の部分クラスとして定義し,そのモデル検査アルゴリズムを開発した.AliasingPDSは,再帰呼び出しとオブジェクトの無制限な動的生成を同時に扱いつつ,到達可能性判定問題が決定可能となるよう設計された実用的かつ強力な計算モデルである.AliasingPDSの上にJavaプログラムをモデル化することで,より現実的なソフトウェアモデル検査法構築の基盤となることが期待される.●モデル検査システムの開発モデル検査システムの木言語処理部(所属判定,積集合演算)に関する基本調査および設計を行った.
英文摘要
本研究では,計算機システムの自動検証技術の1つであるモデル検査法と項書換え系の理論を融合し,一般に無限の状態空間を持つソフトウェアに対しても自動検証できるようモデル検査法を拡張することを目指した.特に本年度は,以下の2点を中心に研究を進めた.●モデル検査可能なクラスの拡張昨年度の研究において研究代表者らは,拡張PDS(LL-GG-TRS)と呼ばれるTRSの部分クラスを定義し,そのLTLモデル検査アルゴリズムを開発した.さらに,拡張PDSを用いることにより,従来検証が困難であった例外処理機能(exception handling)付き再帰プログラムが検証可能となることも発見した.本年度は実用性のさらなる向上を目指し,オブジェクト指向型プログラムをも検証できるよう,新しい計算モデルAliasingPDSをグラフ書換え系の部分クラスとして定義し,そのモデル検査アルゴリズムを開発した.AliasingPDSは,再帰呼び出しとオブジェクトの無制限な動的生成を同時に扱いつつ,到達可能性判定問題が決定可能となるよう設計された実用的かつ強力な計算モデルである.AliasingPDSの上にJavaプログラムをモデル化することで,より現実的なソフトウェアモデル検査法構築の基盤となることが期待される.●モデル検査システムの開発モデル検査システムの木言語処理部(所属判定,積集合演算)に関する基本調査および設計を行った.
期刊论文(4)
专著(0)
科研奖励(0)
会议论文
登录
查看更多内容
情報隠蔽のための自動リファクタリング
自动重构信息隐藏
自动重构信息隐藏
DOI：
--
发表时间：
2005
期刊：
情報処理学会プログラミング研究会
影响因子：
--
作者：
[新田 直也]
通讯作者：
新田 直也
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)
Naoya Nitta、Hiroyuki Seki：“下推系统的扩展及其模型检验方法”第 14 届国际并发理论会议论文集 (CONCUR2003)，LNCS 2761. 281-295 (2003)
Naoya Nitta、Hiroyuki Seki：“下推系统的扩展及其模型检验方法”第 14 届国际并发理论会议论文集 (CONCUR2003)，LNCS 2761. 281-295 (2003)
DOI：
--
发表时间：
期刊：
影响因子：
--
作者：
[]
通讯作者：
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)
Naoya Nitta、Hiroyuki Seki：“下推系统的扩展及其模型检查方法”技术报告 NAIST-IS-TR2003007，奈良科学技术研究所（在网络上发布）。
Naoya Nitta、Hiroyuki Seki：“下推系统的扩展及其模型检查方法”技术报告 NAIST-IS-TR2003007，奈良科学技术研究所（在网络上发布）。
DOI：
--
发表时间：
期刊：
影响因子：
--
作者：
[]
通讯作者：
新田 直也: "Aliasing-PDS : オブジェクト指向プログラムのモデル検査のための新しい計算モデル"シンポジウム「システム検証の科学技術」予稿集. 37-46 (2004)
Naoya Nitta：“Aliasing-PDS：面向对象程序模型检查的新计算模型”“系统验证科学与技术”研讨会论文集 37-46（2004 年）。
Naoya Nitta：“Aliasing-PDS：面向对象程序模型检查的新计算模型”“系统验证科学与技术”研讨会论文集 37-46（2004 年）。
DOI：
--
发表时间：
期刊：
影响因子：
--
作者：
[]
通讯作者：
海外基金