2018 Fiscal Year Annual Research Report
Verification of Web technologies based on the theory of formal languages
| Project/Area Number |
15K00087
|
|---|
| Research Institution | Tokyo Institute of Technology |
|---|
Principal Investigator |
南出 靖彦 東京工業大学, 情報理工学院, 教授 (50252531)
|
|---|
| Project Period (FY) |
2015-04-01 – 2019-03-31
|
| Keywords | ソフトウェア検証 / 形式言語理論 / ウェブ / 正規表現 |
|---|
| Outline of Annual Research Achievements |
ウェブ基盤技術の検証のための基礎理論として以下の研究を行った．
１）Streaming Transducerのコピーに関する制限を緩和したBounded Streaming Transducerに関する研究を行い，合成の具体的構成を与えた．さらに，証明支援系Isabelle/HOLによりBounded Streaming Transducerの形式化を行い，合成の構成の正しさを証明した．
２）ウェブプログラム検証の基盤技術となる文字列制約の充足可能性判定の研究を行った．直線形式(straight-line form)と呼ばれる制限された形式の制約について，Streaming Transducer を用いた充足可能性判定手続きを開発し，プロトタイプ実装を行なった．この充足可能性判定において，Streaming Transducerの合成が重要な役割を果たす．また，Bounded Streaming Trasnducer を用いることで，判定手続きの自然な形式化および実装が可能となっている．
３）先読み付き正規表現に対して微分を導入し，先読み付き正規表現からオートマトンへの変換を与えた．さらに，この変換を精密に分析することで，先読み付き正規表現からオートマトンへの変換の状態数に関する２重指数の上界を与えた．
４）バックトラックによる正規表現マッチングの計算量解析に関して，効率的な判定器を実装する研究を行った．WeberとSeidlによるオートマトンの曖昧度の判定アルゴリズムの手法と本研究で開発してきた文字列から木へのトランスデューサに基づく手法を組み合わせることで効率的な判例アルゴリズムを構築した．これまでの実装でタイムアウトになっていた正規表現についても実用的な時間内での判定が可能となった．
|
