2008 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 |
研究課題を次のサブテーマに分けて研究を推進した。
1.システムを対象とする研究(南出、井田担当),ウェブソフトウェアをシステムとしてモデル化する。今年度はウェブブラウザーのモデル化に取り組んだ。ウェブブラウザーで動作するJavaScriptの挙動が様々な問題を引き起こす要因になっていることから、JavaScriptのモデル化に取り組んだ。特にDOMにアクセスするときの動作がウェブプログラムによって異なることを指摘し、適切なモデル化の必要性を明らかにした
2.ウェブプログラムを対象とする研究(井田、南出担当)プログラムの性質を表す論理式を動的に生成し、生成された論理式の正しさを証明する研究に着手し、この分野における様々なアプローチの調査を行った。この手段として、シリンダー分解やグレブナ基底法、一・リットの方法を掘り下げ適用の可能性を探った。また、プログラムが出力しうる文字列を文脈自由文法を用いて近似するプログラム解析(文字列解析)を応用し、HT肌を生成するプログラムが常に文法的に正しい文書を生成するかを検査する手法を開発した。
3.XMLドキュメントを対象とする研究(鈴木、マリン担当)XML変換言語のパターン照合のための基礎理論について検討を行った。具体的には以下のとおりである。正規表現の積導集合を提案し、それを求めるアルゴリズムと正当性を示した。また正規ヘッジ表現のパターン導集合を提案し、それを用いたパターン照合の正当性、パターン導集合からの有限ヘッジオートマトンとそのオートマトンを用いたパターン照合の正当性を示した。
|
