データ値付きプログラムに対するモデル検査理論の構築と実装
| Project/Area Number |
21J14332
|
|---|
| Research Category |
Grant-in-Aid for JSPS Fellows
|
| Allocation Type | Single-year Grants |
|---|
| Section | 国内 |
|---|
| Review Section |
Basic Section 60010:Theory of informatics-related
|
|---|
| Research Institution | Nagoya University |
|---|
Principal Investigator |
仙田 涼摩 名古屋大学, 情報学研究科, 特別研究員(DC2)
|
|---|
| Project Period (FY) |
2021-04-28 – 2023-03-31
|
| Project Status |
Completed (Fiscal Year 2021)
|
| Budget Amount *help |
¥900,000 (Direct Cost: ¥900,000)
Fiscal Year 2021: ¥500,000 (Direct Cost: ¥500,000)
|
|---|
| Keywords | 形式言語理論 / ソフトウェア工学 / ソフトウェア合成 / レジスタ付き計算モデル |
|---|
| Outline of Research at the Start |
プログラムに含まれるバグを無くし，システムの安全性を確保する研究が近年でも強く求められている．中でも，人間が実装したプログラムにバグが無いかを自動的に確認する「ソフトウェア検証」，仕様書からプログラムを自動生成する「ソフトウェア合成」というアプローチがよく用いられる．プログラムはデータ値(数値情報)を含んでいることが多いが，データ値は一般に無限通りありうることから，データ値に関する条件を検証することが難しかった．本研究では，データ値を扱うことのできる計算モデルである，レジスタ付き計算モデル群を用いた，データ値付きプログラムに関するソフトウェア検証，合成の理論と手法の構築を行う．
|
| Outline of Annual Research Achievements |
プログラムに含まれるバグを無くしてシステムの安全性を確保する手法として、システムに対する入力/出力の制約を記述した仕様書からプログラムを自動生成する「リアクティブ合成」というアプローチがよく知られている。本分野において、「ある計算モデルAによって表現される仕様について、これを満たす実装 Tを構築できるか？」という問題を合成可能性問題と呼ぶ。この問題は、仕様×実装の組が有限オートマトン(NFA)×有限文字列変換器(FT)の場合に決定可能であることが示されているほか、NFAとFTに対してデータ値を扱えるよう拡張したレジスタオートマトン(RA)とレジスタ付き文字列変換器(RT)を仕様、実装とする場合についても考察がなされているが、仕様と実装がプッシュダウンモデルの場合については十分な研究がなされていなかった。
本研究にて、我々はプッシュダウンオートマトン(PDA)×プッシュダウン文字列変換器(PDT)に関する合成可能性問題が、PDAが決定性の場合は指数時間可解、非決定性の場合は決定不能であることを証明した。加えて、PDA、PDTにレジスタを付加して拡張したRPDA、RPDTについても合成可能性問題を考察し、問題が二重指数時間可解となるような制約(visibly決定性)を提案した。また、具体的にvisibly決定性RPDAで表現される仕様を満たす実装であるRPDTが存在する場合に、そのRPDTを構成するアルゴリズムを示した。一般的なプログラムはデータ値、スタック等を含んでいることが多く、これらを扱えるモデルに関する合成可能性問題について考察した本研究の成果を用いることで、より実用的な表現を仕様に許すことが可能になる。
|
| Research Progress Status |
翌年度、交付申請を辞退するため、記入しない。
|
| Strategy for Future Research Activity |
翌年度、交付申請を辞退するため、記入しない。
|
Report
(1 results)
Research Products
(2 results)
