| 研究課題/領域番号 |
15K00087
|
|---|
| 研究機関 | 東京工業大学 |
|---|
研究代表者 |
南出 靖彦 東京工業大学, 情報理工学院, 教授 (50252531)
|
|---|
| 研究期間 (年度) |
2015-04-01 – 2018-03-31
|
| キーワード | ソフトウェア検証 / 形式言語理論 / ウェブ / 正規表現 / プッシュダウンオートマトン |
|---|
| 研究実績の概要 |
ウェブ基盤技術の検証のための基礎理論として以下の研究を行った．
１）インデックスされた重み領域を持つ重み付きプッシュダウンオートマトンの到達可能性判定に関するな研究を行った．この問題の判定アルゴリズムは，先行研究においてHTML5構文解析仕様に対するテストの自動生成に応用されている．本年度には，この判定アルゴリズムの基礎となる理論を整理し，また，この拡張された重み付きプッシュダウンオートマトンの枠組みで，スタックを書き換え可能にしたプッシュダウンオートマトンおよびWell-structured プッシュダウンオートマトンの到達可能性判定アルゴリズムを説明できることを示した．これらの成果をまとめた論文を，学術雑誌Logical Structures in Computer Scienceに出版した．
２）文脈自由言語と超決定性プッシュダウン・オートマトンの受理言語の包含判定問題が決定可能であることの簡明な証明を与えた．これは，超決定性プッシュダウン・オートマトンの受理言語が，ある種のモノイドにより表現できることに基づいており，既存の証明では明らかでなかった本質的な構造を明らかにしている．
３）ウェブシステム基盤の検証に有効であると考えられるStreaming String Transducerに関して，トランスヂューサの合成法の研究を行った．Alurらによる先行研究によって，Streaming Ttransducerが合成に関して閉じていることが示されていたが，詳細な構成法を示されておらず，また，最初に与えらえた構成法に誤りがあることが知られていた．本研究では，この合成の構成法を詳細に定義し，厳密な証明を与えた．
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
HTML5構文解析仕様に対するテスト自動生成に関する研究の基礎となった重み付きプッシュダウンオートマトンの到達可能性解析についての研究成果を論文誌Logical Methods in Computer Scienceにおいて出版した．これは，TACAS2013で発表した先行研究が特集号に招待され，先行研究を発展し纏めたものである．また，ウェブシステム基盤の検証に有効であると考えられるStreaming String Transducerに関して，二つのトランスヂューサの合成の厳密な構成を与えることができた．これは，Streaming String Transducerの理論をウェブシステム基盤の検証へ応用する上で重要なステップとなっている．
|
| 今後の研究の推進方策 |
Streaming Transducerに関する研究については，これまで行ってきた正規表現マッチングの時間計算量解析に関する研究で得られた知見が応用できる見込みである．この知見を適用することで，Streaming Transducerの定義に現れる制限を緩和でき，また，この緩和により合成などの構成法，実装を単純化できる見込みである．また，Streaming Transducerの理論を，ウェブブラウザにおいてクロスサイトスクリプティング対策として用いられているXSSAuditorの定式化，検証に応用する予定である．
来年度が最終年度であるため，国内外の関連分野の研究者との議論を進めることにより，基礎となる理論を整理し，より適用範囲の広い基礎理論の構築を目指す．
|
| 次年度使用額が生じた理由 |
今年度は，学術雑誌論文として成果をまとめることに注力したため，国際会議での発表は行わなかった．そのため，旅費の支出が予定よりも少額となった．
|
| 次年度使用額の使用計画 |
次年度には，早い時期に国際会議等での研究発表を行うことを目指し，次年度に繰り越しとなった助成金は，そのための旅費等に使用する予定である．
|
