2014 Fiscal Year Annual Research Report
| Project/Area Number |
24500028
|
|---|
| Research Institution | University of Tsukuba |
|---|
Principal Investigator |
南出 靖彦 筑波大学, システム情報系, 准教授 (50252531)
|
|---|
| Project Period (FY) |
2012-04-01 – 2015-03-31
|
| Keywords | ソフトウェア検証 / プログラム解析 / ウェブ / 文脈自由文法 / プッシュダウンシステム / HTML5 |
|---|
| Outline of Annual Research Achievements |
文字列解析によるウェブソフトウェア開発支援について以下の研究を行った．
（１）文字列から新たな文字列を生成する計算モデルとしてAlurらにより提案されたストリーミング文字列トランスデューサ(Streaming String Transducer:SST)を，正規表現による文字列置換に関する検証問題に応用した．正規表現による文字列置換を模倣する関数的SSTを構成し，関数的SSTの等価性判定により，その等価性の判定を実現した．また，AlurらによるSSTの等価性判定アルゴリズムを複数のステップに分割・再構成し，より見通しの良い判定アルゴリズムを与えた．
（２）一般化された重みの構造を持つ重み付きプッシュダウンシステムについて，その表現力を明らかにする研究を行い，次の二つのプッシュダウンシステムの拡張を表現できることを示した：Well Structured Pushdown System（well-quasi orderを備えた無限集合をスタック記号として許す拡張）, スタック全体をトランスデューサによって書き換えることを許す拡張．
（３）正規表現マッチングの計算量判定について研究を行った．トップダウントランスデューサに関するAhoとUllmanによる判定アルゴリズムが，先読み付きトップダウントランスデューサに拡張できるかについて分析を行った．この拡張が実現できれば，2乗や3乗などのオーダに対して計算量の判定が可能となり，正規表現マッチングが原因となるDoS脆弱性をより詳細に検査できるようになる．
|
