2016 Fiscal Year Annual Research Report
高レベル言語で記述されたソフトウェアの時相的・関係的仕様の検証
| Project/Area Number |
16H05856
|
|---|
| Research Institution | University of Tsukuba |
|---|
Principal Investigator |
海野 広志 筑波大学, システム情報系, 助教 (80569575)
|
|---|
| Project Period (FY) |
2016-04-01 – 2020-03-31
|
| Keywords | リファインメント型 / 依存型 / 関係的仕様 / 時相的仕様 / ホーン節制約解消 / プログラム検証 / 帰納的定理証明 |
|---|
| Outline of Annual Research Achievements |
本研究では、研究代表者がこれまでに研究・開発を行ってきた高レベル言語のための検証理論であるリファインメント型システムおよびホーン節制約解消法、関数型言語 OCaml のための全自動・高精度検証ツールである RCaml を発展させ、実用上重要であるにも関わらず既存手法では十分に扱えなかった言語機能（再帰データ構造・参照セル・オブジェクト・モジュール機構・例外処理機構・マルチスレッド機構）および仕様（時相的仕様・関係的仕様）の全自動・高精度検証法の確立を目指している。本年度は以下の成果を得た。
１．再帰データ構造を扱うプログラムを高精度に検証できるようリファインメント型システムを拡張した上で、再帰データ構造によるオブジェクトのエンコード法を考案・実装することによって、オブジェクトを扱うプログラムの高精度検証を実現した。さらに、ホーン節制約解消法を代数データ構造を扱えるよう拡張することによって、拡張された型システムのための型推論を実現し、全自動・高精度検証を可能とした。
2. 無交代様相μ計算の論理式として記述された時相的仕様の検証のために、論理式と検証対象の高レベルプログラムの積をとることによって得られる無限状態 Buechi ゲームを、RCaml が扱える停止性・非停止性検証問題に帰着して解く手法を考案・実装した。
3. 高レベルプログラムの関係的仕様検証のため、帰納的定理証明に基づくホーン節制約解消法を拡張して、ヒープ制約の解消、関係的プログラム合成、余帰納法の自動化を実現した。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
研究実績の概要で述べたとおり、リファインメント型システムおよびホーン節制約解消法の拡張の柱となる部分については順調に進展している。一方、本年度中の実施を予定していた、例外処理機構・マルチスレッド機構の再帰データ構造を用いたエンコード法の確立や、一般の様相μ計算の論理式として記述された時相的仕様の検証といった発展的な研究については当初の計画より遅れている。その理由は平成29年度以降に実施を予定していた関係的仕様検証のための拡張を前倒しして実施したためであり、そちらに関してはシステム検証に関するトップ会議であるCAVに論文が採択されるなど顕著な成果が得られている。
|
| Strategy for Future Research Activity |
現在までの進捗状況で述べたように、平成28年度中に実施を予定していた研究計画と平成29年度以降に予定していた計画が一部入れ替わってはいるが、今後も予定通り研究を推進していく。
|
