Software Verification Based on the Theory of Transducers
| Project/Area Number |
19K11899
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Multi-year Fund |
|---|
| Section | 一般 |
|---|
| Review Section |
Basic Section 60050:Software-related
|
|---|
| Research Institution | Tokyo Institute of Technology |
|---|
Principal Investigator |
南出 靖彦 東京工業大学, 情報理工学院, 教授 (50252531)
|
|---|
| Project Period (FY) |
2019-04-01 – 2024-03-31
|
| Project Status |
Granted (Fiscal Year 2022)
|
| Budget Amount *help |
¥3,770,000 (Direct Cost: ¥2,900,000、Indirect Cost: ¥870,000)
Fiscal Year 2022: ¥650,000 (Direct Cost: ¥500,000、Indirect Cost: ¥150,000)
Fiscal Year 2021: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000)
Fiscal Year 2020: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000)
Fiscal Year 2019: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000)
|
|---|
| Keywords | ソフトウェア検証 / トランスデューサ / 形式言語 / 文字列制約 / オートマトン / 形式言語理論 |
|---|
| Outline of Research at the Start |
ソフトウェア検証の基盤となる理論として，これまで主に出力を持たないオートマトンなどの計算モデルが用いられてきたが，ソフトウェア検証において出力を持つ計算モデルすなわちトランスデューサの理論が重要になってきている. 本研究はトランスデューサとその拡張のソフトウェア検証への応用を進め，検証精度の向上，検証で扱えるプログラムの性質の拡張などにおいてソフトウェア検証の深化を目指す．特に，以下の３つの課題に取り組む：トランスデューサを含む文字列制約の充足可能性判定手続き，木トランスデューサ理論に基づくプログラムの時間計算量解析，ウェブブラウザにおけるセキュリティ対策機構のトランスデューサを用いた検証．
|
| Outline of Annual Research Achievements |
本年度には，以下の研究を行なった．
＊ 後方参照を含む拡張正規表現マッチングの計算量解析の研究を継続した．解析の精度を改善するため，集合と木のモナドを組み合わせたモナドを用いるアプローチについて研究を進め，正規表現の微分の考え方を全体に適用することで，これまでより精度の高い解析を実現した．これまでの研究で実装した解析器に本方式を実装し，既存の解析結果と比較した結果，全体の3 分の1 近くの正規表現でオーダの次数が1 以上下がっており, 解析精度が向上されていることを確認できた. 解析の後半は，Berglund らによる非決定性トランスデューサの出力増加率判定に基づいているが，解析内で用いられる複数の変換を組み合わせて単純化するなどの改良を行なった．
＊ 先読み付き文脈自由文法は文脈自由文法と解析表現文法（PEG）の両方を拡張したものである．本年度の研究では，まず，先読み付き言語の区間に基づく意味論を導入した．この区間による意味論は，3値論理に基づく意味論に理論的には完全に対応するものであるが，より形式言語理論の古典的な意味論に近いものになっている．また，先読み付き正規表現の微分を先読み付き文脈自由文法の微分に拡張し，微分による所属判定の計算量が文字列長nに対して，O(n^3)となることを示した．
＊ トランスデューサを用いたソフトウェア検証の基礎として，自然言語で書かれた仕様を自然言語処理を用いて形式化する研究を行なった．古典的な半単一化を用いた処理と，Transformer を用いた機械翻訳を組み合わせることで，HMTL5字句解析仕様の主要部分を形式化することができた．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
拡張正規表現マッチングの計算量解析においては，2021年度までの研究で先読み付き決定性トランスデューサの出力増加率解析を用いた計算量解析手続きの構築と判定器の実装ができており一定の成果が得られていた．今年度には，後方参照を含む正規表現について，非決定性トランスデューサの出力増加率解析を用いることで精度の改善することができた．非決定性トランスデューサを用いた解析の枠組みはより適用範囲が広く，今後の応用が見込める．
先読み付き文脈自由文法に関する研究は，閉包性，微分，所属判定など主要な理論的な性質を解明が本年度の研究までに完了している．未解決の問題としては，任意の先読み付き文脈自由文法を任意の語に対して，所属，非所属が決まる文法に変換できるかがあるが，非常に難しい問題と考えている．
|
| Strategy for Future Research Activity |
これまでの研究で整数引数を持つ文字列演算を含む文字列制約の充足可能性判定手続きを設計し，その実装と評価を行なってきた．今後は，この充足可能性判定の実用性を高めるために，Parikhオートマトンの空性判定の効率的な実装の研究を行う予定である．SMTソルバーの代わりに整数計画法のソルバーを用いることを検討している．
|
Report
(4 results)
Research Products
(20 results)
