データ値付きプログラムに対するモデル検査理論の構築と実装

プログラムに含まれるバグを無くしてシステムの安全性を確保する手法として、システムに対する入力/出力の制約を記述した仕様書からプログラムを自動生成する「リアクティブ合成」というアプローチがよく知られている。本分野において、「ある計算モデルAによって表現される仕様について、これを満たす実装 Tを構築できるか？」という問題を合成可能性問題と呼ぶ。この問題は、仕様×実装の組が有限オートマトン(NFA)×有限文字列変換器(FT)の場合に決定可能であることが示されているほか、NFAとFTに対してデータ値を扱えるよう拡張したレジスタオートマトン(RA)とレジスタ付き文字列変換器(RT)を仕様、実装とする場合についても考察がなされているが、仕様と実装がプッシュダウンモデルの場合については十分な研究がなされていなかった。本研究にて、我々はプッシュダウンオートマトン(PDA)×プッシュダウン文字列変換器(PDT)に関する合成可能性問題が、PDAが決定性の場合は指数時間可解、非決定性の場合は決定不能であることを証明した。加えて、PDA、PDTにレジスタを付加して拡張したRPDA、RPDTについても合成可能性問題を考察し、問題が二重指数時間可解となるような制約(visibly決定性)を提案した。また、具体的にvisibly決定性RPDAで表現される仕様を満たす実装であるRPDTが存在する場合に、そのRPDTを構成するアルゴリズムを示した。一般的なプログラムはデータ値、スタック等を含んでいることが多く、これらを扱えるモデルに関する合成可能性問題について考察した本研究の成果を用いることで、より実用的な表現を仕様に許すことが可能になる。

プログラムに含まれるバグを無くしてシステムの安全性を確保する手法として、システムに対する入力/出力の制約を記述した仕様書からプログラムを自動生成する「リアクティブ合成」というアプローチがよく知られている。本分野において、「ある計算モデルAによって表現される仕様について、これを満たす実装 Tを構築できるか？」という問題を合成可能性問題と呼ぶ。この問題は、仕様×実装の組が有限オートマトン(NFA)×有限文字列変換器(FT)の場合に決定可能であることが示されているほか、NFAとFTに対してデータ値を扱えるよう拡張したレジスタオートマトン(RA)とレジスタ付き文字列変換器(RT)を仕様、実装とする場合についても考察がなされているが、仕様と実装がプッシュダウンモデルの場合については十分な研究がなされていなかった。本研究にて、我々はプッシュダウンオートマトン(PDA)×プッシュダウン文字列変換器(PDT)に関する合成可能性問題が、PDAが決定性の場合は指数時間可解、非決定性の場合は決定不能であることを証明した。加えて、PDA、PDTにレジスタを付加して拡張したRPDA、RPDTについても合成可能性問題を考察し、問題が二重指数時間可解となるような制約(visibly決定性)を提案した。また、具体的にvisibly決定性RPDAで表現される仕様を満たす実装であるRPDTが存在する場合に、そのRPDTを構成するアルゴリズムを示した。一般的なプログラムはデータ値、スタック等を含んでいることが多く、これらを扱えるモデルに関する合成可能性問題について考察した本研究の成果を用いることで、より実用的な表現を仕様に許すことが可能になる。