2009 Fiscal Year Annual Research Report
記号計算の理論を駆使したウェブソフトウェアのモデル化と検証
| Project/Area Number |
20300001
|
|---|
| Research Institution | University of Tsukuba |
|---|
Principal Investigator |
井田 哲雄 University of Tsukuba, 大学院・システム情報工学研究科, 教授 (70100047)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
南出 靖彦 筑波大学, 大学院・システム情報工学研究科, 准教授 (50252531)
MARIN Mircea 筑波大学, 大学院・システム情報工学研究科, 講師 (60396603)
鈴木 大郎 会津大学, コンピュータ理工学部, 准教授 (90272179)
|
|---|
| Keywords | 情報基礎 / ソフトウェア学 / 記号計算 / ウェブ |
|---|
| Research Abstract |
ウェブシステムを対象とする研究,ウェブプログラムを対象とする研究,XMLドキュメントを対象とする研究に研究課題を整理し,それぞれについて研究を推進し,以下の成果を得た.
・webEosとよぶ,計算折紙構築および定理証明のための記号計算サービスのシステムの拡張・改良を行いつつ,ソフトウェアのセキュリティの問題点の解明や,性能改善の可能性について検討した.
・Hoare論理やSATを用いてプログラムの性質を検証する研究について,研究の現状をサーベイしつつ,これら研究においてシリンダー分解やグレブナ基底計算等の記号計算アルゴリズの適用手法について考察した.
・ウェブソフトウェアで用いられる文字列解析のアルゴリズムについて考察し,解析精度を改善した.
・ウェブソフトウェアで広く用いられる言語Rubyの操作的意味論と制御フロー解析の研究を行い,高い精度のプログラム解析を実現した.また制御フロー解析の健全性を,操作的意味論に基づき証明した.
・XML文書の妥当性検証を正則生垣言語を介して行った.また,正規表現パターンを正則生垣言語で表現するために用いる方法の研究を行った.
・XML文書と変換規則のパターンとのパターン照命のための理論に関する研究を行い,正規生垣言語表現のデリバティブを計算するだけで、ヘッジ(生垣,XML文書)とヘッジパターンとの照合が可能になることを示した.また、ヘッジ書換え系の形で複数の変換規則が与えられたときに、ヘッジとのパターン照合が成功する変換規則を効率よく見つけるための方法を考案した.
|
Research Products
(7 results)
