定式化された形式木言語理論に基づくソフトウェア基盤技術の開発
| Project/Area Number |
17K00007
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Multi-year Fund |
|---|
| Section | 一般 |
|---|
| Research Field |
Theory of informatics
|
|---|
| Research Institution | Tohoku University (2018-2019)
The University of Electro-Communications (2017) |
|---|
Principal Investigator |
中野 圭介 東北大学, 電気通信研究所, 教授 (30505839)
|
|---|
| Project Period (FY) |
2017-04-01 – 2021-03-31
|
| Project Status |
Granted (Fiscal Year 2019)
|
| Budget Amount *help |
¥4,420,000 (Direct Cost: ¥3,400,000、Indirect Cost: ¥1,020,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)
Fiscal Year 2018: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000)
Fiscal Year 2017: ¥1,300,000 (Direct Cost: ¥1,000,000、Indirect Cost: ¥300,000)
|
|---|
| Keywords | 形式木言語理論 / 木トランスデューサ / プログラム検証 / 等価性判定 / 型検査 / 双方向変換 / 木オートマトン / 結合子論理 / 定理証明支援系 / プログラム変換 / ソフトウェア検証 |
|---|
| Outline of Annual Research Achievements |
本研究の目的は定式化された形式木言語理論をソフトウェア基盤技術へ応用することである． 3年目にあたる令和元年度では，木構造データ変換の形式モデルである木トランスデューサについて研究を進めた．主な成果は，研究代表者がこれまでに研究を進めてきたスタックを用いた木トランスデューサの延長となるものであり，(1)木トランスデューサの等価性判定に関する結果と(2)既存の木トランスデューサのクラスに対するスタック機構の導入である．
(1)の木トランスデューサの等価性判定についての結果は，ここ数年で明らかになった「文字列から木への下降型木変換器」に対する等価性判定アルゴリズムを応用するものである．具体的には，スタックを用いた効率のよい木構造処理を直接表現した木変換のクラス「ストリーム型木トランスデューサ」を扱い，スタックを扱うクラスのトランスデューサのうち，等価性判定のアルゴリズムが存在する最も汎用的なクラスの発見に成功した．
(2)の木トランスデューサのクラスの拡張においては，研究代表者が提案した属性付き木トランスデューサに対するスタック機構の導入を応用し，マクロ木トランスデューサと呼ばれる上位のクラスに対して同様の拡張を行った．本研究により，スタック機構の導入した場合には，この下位と上位のクラス関係が必ずしも成立しなくなる可能性があることを確認した．
この他の成果として，研究代表者のテーマの一つであった木構造データに対する双方向変換についての研究も並行して進めた．双方向変換は，二つのデータ間を同期するために必要な二つの変換のことであるが，それらの一貫性を保証するために必要な複数の双方向変換則に対し，これまで知られていなかった相互の関係を発見した．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
本研究の最終的な目標は，形式木言語理論をソフトウェア基盤技術へ応用することであり，その応用は主に (i)プログラム検証 と (ii)プログラム効率化 の二つであった．昨年度提示した計画では，本年度は(i)について重点的に取り組み，特に木トランスデューサの型検査とよばれる入出力仕様に対する整合性検査について研究を進める予定であったが，スタック機構で拡張された木トランスデューサの型検査については，逆像の正規保存性が成り立たないために従来の手法がそのまま適用できないが，特殊な場合に限定した場合には型検査も可能であることが確認された．一方，単純化されたスタック機構を扱う木トランスデューサについては，型検査（すべての入力について出力が仕様を満たすことの検査）よりも厳格である等価性判定（すべての入力について二つの変換の出力が等しくなることの検査）について新たな発見があり，そのアルゴリズムについて研究を進めてきた．さらに，当初の計画で予期していなかった双方向変換との関係も確認され，来年度以降の新たな研究課題として進めていくことが期待される． 以上のことから，現在までの進捗状況として，最終目標に向かって順調に進めることができていると言える．
|
| Strategy for Future Research Activity |
当初の計画においては，3年め以降においてはプログラム合成やモデル検査などの高信頼ソフトウェア技術への応用に必要な木トランスデューサおよび木オートマトンの拡張も進めていく予定であった．最終年度においては，これまでの研究経過や発見を踏まえ，形式木言語理論に対して更なる応用に取り組む．特に，双方向変換技術や等価性判定への応用について研究を行う．双方向変換技術への応用は当初の計画にはなかったものであるが，形式木言語理論や関連する枠組みの新たな応用として研究を実施する．
双方向変換技術は，データベースの分野でビュー更新問題として1980年代から研究が進められてきたが，21世紀に入ってから言語的アプローチによって新たな見方が導入され，近年では盛んに研究されている分野となっている．研究代表者は，形式木言語理論の立場から木構造データ変換に対する双方向変換について研究してきた経験を生かし，昨年度において双方向変換技術を再訪した結果，これまで知られていなかった双方向変換の一貫性の判定方法について新たな知見を得た．来年度においては，この知見を発展させ，満たすべき一貫性の本質について形式化を行う．
また，等価性判定が可能なストリーム木変換のクラスについても精査を行い，より一般的なクラスにおいて等価性判定が決定可能になるかを確認し，応用のための実装を進める．
|
Report
(3 results)
Research Products
(19 results)
