| 研究課題/領域番号 |
16H05856
|
|---|
| 研究機関 | 筑波大学 |
|---|
研究代表者 |
海野 広志 筑波大学, システム情報系, 准教授 (80569575)
|
|---|
| 研究期間 (年度) |
2016-04-01 – 2020-03-31
|
| キーワード | リファインメント型 / 依存型 / 時相的仕様 / 関係的仕様 / ホーン節制約解消 / プログラム検証 / プログラム合成 / 動的論理 |
|---|
| 研究実績の概要 |
本研究では、研究代表者がこれまでに研究・開発を行ってきた高レベル言語のための検証理論であるリファインメント型システムおよびホーン節制約解消法、関数型言語 OCaml のための全自動・高精度検証ツールである RCaml を発展させ、実用上重要であるにも関わらず既存手法では十分に扱えなかった言語機能（再帰データ構造・参照セル・オブジェクト・モジュール機構・例外処理機構・マルチスレッド機構）および仕様（時相的仕様・関係的仕様）の全自動・高精度検証法の確立を目指している。本年度は以下の成果を得た。(1) 分岐仕様の検証のためのリファインメント型システムを提案し、そのメタ理論を整備した。(2) 依存時相仕様の検証のためのリファインメント型システムを提案し、型検査問題が不動点述語論理の妥当性判定問題に帰着されることを示した。さらに、妥当性判定のための演繹体系を提案した。また、型システムおよび演繹体系のメタ理論を整備した。(3) 高階プログラムの時相仕様記述のための動的命題論理HOT-PDLを提案し、そのセキュリティおよびリファインメント型検査への応用を示した。さらに、高階プログラムに対するHOT-PDLモデル検査問題の決定可能性を示した。(4) 昨年度までに得られた成果である帰納的定理証明に基づくホーン節制約解消法を拡張し、余帰納的述語を扱えるようにし、プログラムの双模倣性自動検証への道筋をたてた。(5) 帰納的定理証明に基づくホーン節制約解消法を拡張し、関係的仕様からのプログラム合成を可能とした。(6) リファインメント型システムと分離論理およびホーア型理論を融合することによって、破壊的変更が可能なデータ構造を扱うプログラムの検証をヒープの理論H上のホーン節制約解消に帰着する手法を考案した。さらに、帰納的定理証明に基づくホーン節制約解消法を拡張することによって、ヒープの理論H上のホーン節制約解消を可能にした。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
1: 当初の計画以上に進展している
理由
研究実績の概要で述べたとおり、リファインメント型システム、ホーン節制約解消、および時相仕様記述のための論理に関する研究で大きな成果を得ている。特に研究実績の概要で述べた成果1,2,3については、それぞれプログラミング言語のトップ会議POPL、計算機科学における論理のトップ会議LICS、システム検証のトップ会議CAVに論文が採択されている。さらに4,5については国内の研究大会（日本ソフトウェア科学会第34回大会）において学生がそれぞれ学生奨励賞と優秀発表賞を受賞している。
|
| 今後の研究の推進方策 |
今後も計画通り研究を推進する。平成30年度には、昨年度までに得られたリファインメント型システムに関する研究成果に基づき、OCaml言語用検証ツールRCamlを拡張することによって、高階・再帰データ構造、参照セル、オブジェクト、モジュール機構、例外処理機構、マルチスレッド機構といった高度な言語機能を扱うプログラムの半自動検証を実現する。それと並行して、Java言語用検証ツールのプロトタイプ開発を行う。さらに、リファインメント型システムを拡張し、様相μ計算で記述された時相的仕様を完全に扱えるようにする。
平成31年度には、ホーン節制約および不動点述語論理制約の自動解消法について研究し、OCamlプログラムおよびJavaプログラムの時相的・関係的仕様の全自動検証を実現する。その上で、関係的仕様と時相的仕様を真に包含する仕様クラスであるHyperpropertiesの全自動検証も実現し、情報セキュリティ（機密性・完全性・可用性）への応用を行う。
|
