2013 Fiscal Year Research-status Report
検証技術と非標準型体系を用いたモデル検査器コンパイラの進化的発展
| Project/Area Number |
24650016
|
|---|
| Research Institution | Waseda University |
|---|
Principal Investigator |
上田 和紀 早稲田大学, 理工学術院, 教授 (10257206)
|
|---|
| Keywords | モデル検査 / コンパイラ / 検証 / 型体系 / ソフトウェア進化 |
|---|
| Research Abstract |
階層グラフ書換えに基づくモデリング言語LMNtalは，高水準言語プログラムが直接モデル検査できる処理系をもつことを特徴とする．ソフトウェア検証系として，LMNtal処理系自体の正当性を検証することは重要かつ基本的な要請であるが，グラフ書換え言語プログラムの抽象機械コードへのコンパイルは大きなセマンティックギャップの橋渡し作業であり，信頼性と保守性の改善が強く求められている．本年度は，モデル検査器コンパイラの信頼性と保守性の改善に向けて，以下の研究開発を進めた．
1. 処理系の単純さと信頼性向上のために前年度提案した，リンクの互換に基づくグラフ書換えを実現する抽象機械について，新たに導入した命令を実行時処理系slimに実装するとともに，抽象機械へのコンパイラの整備を進めた．
2. より高い表現力をもつハイパーグラフ書換えに進化させるべく，抽象機械およびコンパイラの拡張を行った．また，多相ラムダ計算の型体系の記述実験を通じて拡張機能の妥当性を確認し必要な改良を行った．
3. リンク互換操作を導入した抽象機械におけるグラフ書換え操作の形式化と種々の性質証明を，定理証明支援系Coqを用いて行った．まず，グラフ構造と基本的な書換え命令の動作をCoq上で形式化した．グラフ構造の定義は，書換え操作を厳密に論じることができるように，実装に近い構造を選択した．次に，形式化した定義の上で成り立ついくつかの重要な性質，すなわち (i) 形式化した各グラフ書換え命令の形式的仕様，および (ii) LMNtalグラフのwell-formedness保存定理を証明した．実装レベルのデータ構造はLMNtalグラフとみなせない不正な構造も含むので，各命令におけるwell-formednessの保存は，命令列の実行の安全性を論じる上で重要な性質である．この作業を通じて221個の定理を証明し，証明スクリプトは全体で4100行におよんだ．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
平成25年度の研究実施計画のうち「コード生成器の記述と検証」については、グラフのマッチングと書換えのうちの後者に絞って、個々の抽象機械命令の定式化と性質検証を着実に進め、証明支援系の活用法を含めて多くの知見を得ることができた。また、前年度に設計した高抽象度の抽象機械命令の実装を進めた。
一方、抽象機械の命令列の検証をはじめとするより上位の検証は今後の課題となった。
もう一つの項目である「静的型体系」については平成24年度に前倒しで研究を進めてハイパーリンクを扱う型体系を構築したが、平成25年度は、例題記述を中心としたハイパーリンク機能の妥当性評価を主に進めてきた。
|
| Strategy for Future Research Activity |
平成25年度までの研究によって、グラフ書換えに基づくモデル検査器コンパイラの検証作業の規模感がつかめてきた。本萌芽研究の範囲では、コンパイラの各フェーズのうち、グラフ書換え操作に絞っての正当性検証への道筋をつけることを目標とする。
一方、コンパイラ全体の進化の観点からは、大学院生の協力を得ながら、高抽象度の抽象機械命令の採用をはじめとする種々の技法によって、信頼性と保守性の改善をさらに推進する。
|
| Expenditure Plans for the Next FY Research Funding |
仮想機械命令の検証のための研究協力者への謝金が増加し、単年度ではほぼ当初計画通りの支出があったものの、初年度の未使用額がほぼそのまま第３年度に送られることとなった。
これまでの成果と蓄積に基づき、グラフ書換えに基づくモデル検査器コンパイラの全体の整備をさらに加速させる。このための謝金や計算機用品の支出を当初計画よりも増強する予定である。
|
