2011 Fiscal Year Annual Research Report
記号計算の理論を駆使したウェブソフトウェアのモデル化と検証
| Project/Area Number |
20300001
|
|---|
| Research Institution | University of Tsukuba |
|---|
Principal Investigator |
井田 哲雄 筑波大学, システム情報系, 教授 (70100047)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
南出 靖彦 筑波大学, システム情報系, 准教授 (50252531)
鈴木 大郎 会津大学, コンピュータ理工学部, 准教授 (90272179)
|
|---|
| Keywords | 情報基礎 / ソフトウェア / 記号計算 / ウェブ / 検証 |
|---|
| Research Abstract |
本年度は研究課題を次の3点に絞って,研究を推進した.
(1)文字列解析によるウェブプログラム検証の研究を継続した.プログラミング言語で用いられる正規表現マッチングの意味論の研究を継続し,前年度に構築したモナドを用いた意味論を,モナドモルフィズム,モナドトランスフォーマを用いて再構成し,より洗練された意味論を構築した.また,データベースとの連携の解析を導入することにより,文字列解析による蓄積型クロスサイトスクリプティング脆弱性検査を実現した.(2)ポジションオートマトンとよばれるオートマトンを利用した,正規表現の貪欲マッチングのためのアルゴリズムの設計とその実装を行った.このオートマトンの各遷移に正規表現中のキャプチャの位置を表すタグを付加した.それをもとにアルゴリズムの設計とC++による実装を行った.その結果いくつかの場合でFrischとCardelliによる効率のよいマッチングアルゴリズムの速度を大きく上回る結果が得られた.(3)WebEos(Web E-Origami Systemの略)と呼ぶウェブを介して稼働するソフトウェアを開発してきたが,今年度も,このソフトウェアの改良とその核となる部分の形式化を進めた.核となる部分は,藤田の基本操作と呼ばれるセットをプログラム化したものであり,この形式化と様々な性質の検証が非常に重要であった.これを,証明支援系Isabelle/HOLを用いて行った.検証には,記号論理的な知見と代数的な知見を組み合わせることが不可欠であるが,既存の証明支援系は,前者では満足すべき能力を有するものの,後者は比較的弱く,研究の推進には困難が伴った。幾何と代数の基本的なところは独自の証明スクリプトをベースにするのではなく,記号代数系Mathematicaの計算結果を援用した.これらの研究成果により,既に稼働しているソフトウェアの改善及び機能の向上が得られた.
|
