2013 Fiscal Year Research-status Report
| Project/Area Number |
24500028
|
|---|
| Research Institution | University of Tsukuba |
|---|
Principal Investigator |
南出 靖彦 筑波大学, システム情報系, 准教授 (50252531)
|
|---|
| Keywords | ソフトウェア検証 / プログラム解析 / ウェブ / 文脈自由文法 / プッシュダウンシステム / HTML5 |
|---|
| Research Abstract |
文字列解析によるウェブソフトウェア開発支援について以下の研究を行った．
（１）HTML5構文解析仕様の形式化に基づき，構文解析器のテストのためのHTML文書を自動生成する研究を行った．本年度は，対象とする仕様のサブセットを広げた，特に，active formatting elementと呼ばれる要素に対し，ネストの深さを制限することで，テストの自動生成を可能にした．この拡張を実装し実験を行った結果，HTML5構文解析ライブラリの主要な実装である. html5lib及びgumboについて，非互換性を発見し問題点を開発者に報告した．
（２）HTML5構文解析仕様など，スタックの内部を書き換えるシステムの検証のために，プシュタウンシステムにおいて，スタック内部の書き換えを許す拡張を提案した．拡張したプッシュダウンシステムは，出力付きオートマトン（トランスデューサ）により，スタック内部を書き換える．特に，遷移に用いられるトランスデューサが，合成と商(quotient)に関して閉じている場合には，到達可能性解析が決定可能であることを示した．これにより，この計算モデルをシステム検証に応用することが可能になる．
（３）ウェブソフトウェアで用いられる正規表現マッチングに関する研究を行った．プログラミング言語における正規表現マッチングは，バックトラックに基づき実装されており最悪の場合には実行が指数関数時間となる．近年, この実行時間に関する問題が，DoS脆弱性などの大きな問題の原因となることが報告されている．この問題を解決するため，本研究では，正規表現マッチングの実行が線形時間となるか判定するアルゴリズムを開発した．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
理論面では，スタック内部の書き換えを許すプッシュダウンシステムを提案し，国際会議において発表している．
また，ウェブプログラミングで重要となる正規表現マッチングの実行時間が線形であるかの判定は，実用上非常に有用であり，また，トランスデューサの理論を適用した点でも新規性が高い．
|
| Strategy for Future Research Activity |
文脈自由言語及びプッシュダウンシステムに基づくシステム検証の理論に関する研究を行い，同時に，その成果をウェブソフトウェア開発支援に応用する研究を行う．国際会議などへの参加により，国内外の関連分野の研究者との交流を進め，研究を加速する．
|
| Expenditure Plans for the Next FY Research Funding |
以下の二つの理由から差額が生じた．平成25年度中に購入を計画していた大容量のメモリを持つコンピュータの納品が年度内に間に合わなかった．採録された論文の掲載料の支出が平成26年度に持ち越された．
平成26年度の早い時期に大容量のメモリを持つコンピュータを購入し大規模な実験を行い，研究を進める．
|
