研究課題
特別研究員奨励費
プログラムに含まれるバグを無くし，システムの安全性を確保する研究が近年でも強く求められている．中でも，人間が実装したプログラムにバグが無いかを自動的に確認する「ソフトウェア検証」，仕様書からプログラムを自動生成する「ソフトウェア合成」というアプローチがよく用いられる．プログラムはデータ値(数値情報)を含んでいることが多いが，データ値は一般に無限通りありうることから，データ値に関する条件を検証することが難しかった．本研究では，データ値を扱うことのできる計算モデルである，レジスタ付き計算モデル群を用いた，データ値付きプログラムに関するソフトウェア検証，合成の理論と手法の構築を行う．
プログラムに含まれるバグを無くしてシステムの安全性を確保する手法として、システムに対する入力/出力の制約を記述した仕様書からプログラムを自動生成する「リアクティブ合成」というアプローチがよく知られている。本分野において、「ある計算モデルAによって表現される仕様について、これを満たす実装 Tを構築できるか？」という問題を合成可能性問題と呼ぶ。この問題は、仕様×実装の組が有限オートマトン(NFA)×有限文字列変換器(FT)の場合に決定可能であることが示されているほか、NFAとFTに対してデータ値を扱えるよう拡張したレジスタオートマトン(RA)とレジスタ付き文字列変換器(RT)を仕様、実装とする場合についても考察がなされているが、仕様と実装がプッシュダウンモデルの場合については十分な研究がなされていなかった。本研究にて、我々はプッシュダウンオートマトン(PDA)×プッシュダウン文字列変換器(PDT)に関する合成可能性問題が、PDAが決定性の場合は指数時間可解、非決定性の場合は決定不能であることを証明した。加えて、PDA、PDTにレジスタを付加して拡張したRPDA、RPDTについても合成可能性問題を考察し、問題が二重指数時間可解となるような制約(visibly決定性)を提案した。また、具体的にvisibly決定性RPDAで表現される仕様を満たす実装であるRPDTが存在する場合に、そのRPDTを構成するアルゴリズムを示した。一般的なプログラムはデータ値、スタック等を含んでいることが多く、これらを扱えるモデルに関する合成可能性問題について考察した本研究の成果を用いることで、より実用的な表現を仕様に許すことが可能になる。
翌年度、交付申請を辞退するため、記入しない。
すべて 2021
すべて 雑誌論文 (1件) (うち査読あり 1件、 オープンアクセス 1件) 学会発表 (1件) (うち国際学会 1件)
IEICE Transactions on Information and Systems
巻: E104.D 号: 12 ページ: 2131-2144
10.1587/transinf.2020EDP7265
130008123331
