| 研究課題/領域番号 |
24650016
|
|---|
| 研究種目 |
挑戦的萌芽研究
|
| 研究機関 | 早稲田大学 |
|---|
研究代表者 |
上田 和紀 早稲田大学, 理工学術院, 教授 (10257206)
|
|---|
| 研究期間 (年度) |
2012-04-01 – 2015-03-31
|
| キーワード | モデル検査 / コンパイラ / 検証 / 型体系 / ソフトウェア進化 |
|---|
| 研究概要 |
階層グラフ書換えに基づくモデリング言語LMNtalは，高水準言語プログラムが直接モデル検査できる処理系をもつことを特徴とする．そのコンパイラの正当性の保証はモデル検査器の正当性にかかわる重要な技術課題となるが，グラフ書換え言語プログラムの抽象機械コードへのコンパイルは大きなセマンティックギャップの橋渡し作業であり，信頼性と保守性の改善が強く求められていた．そこで，モデル検査器コンパイラの信頼性と保守性の改善に向けて，本年度は，以下の二つの視点から基礎検討を行った．
1. これまでの抽象機械は，無方向リンクによって形成されるグラフの書換え作業を，手続き型言語におけるポインタ代入に近いレベルの操作列で扱っており，過去の処理系は修正困難な問題点をかかえていた．そこで，リンクの代入ではなくリンクの互換 (exchange) に基づくグラフ書換え作業の実現方法を，LMNtalの意味論との整合性や中間コード生成法などの観点から検討し，膜をもたないLMNtalサブセットに対して新たなコンパイル手法を確立した．
2. モデル検査の空間効率や時間効率の改善に型体系が果たすと期待される役割は大きいが，これまで，LMNtalの型体系の提案はあったもののコンパイラとの連携はとられてこなかった．そこで，最近仕様が確立し処理系の稼働も始まっているHyperLMNtal（ハイパーリンクの導入によるLMNtalの拡張）に対する型体系を新たに設計した．この型体系は，実数領域 [-1,+1] で表現されるケイパビリティの概念を用いてリンクおよびハイパーリンクの向きを表す．本年度はこの型体系の定式化を行うとともに，いくつかのプログラムに対する型推論などを通じて，その設計の妥当性確認を行った．
また今後のコンパイラ進化に備えて，既存のLMNtalコンパイラのコードレビューを行い，本質的な部分の抽出を行った．
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
今後のソフトウェア進化の準備としての既存コンパイラの整備，抽象機械語の再検討，型体系の設計などの点で順調に研究が進展した．今後のコンパイラ進化のためには，抽象機械語の形式化と，それに基づく書換え型言語コンパイラの正当性検証の枠組みが必要となるが，それらの研究開発が今後の重要課題となってきた．
|
| 今後の研究の推進方策 |
証明支援系を用いた書換え型言語コンパイラの記述と検証は高度に挑戦的な課題である．本年度の研究でその出発点につくための諸整備が進んだので，次年度は実際のコンパイラの記述と検証について，段階を追って研究開発を進めてゆきたい．また型体系については，コンパイラへの統合を視野に入れつつ，実装と妥当性評価を進めてゆきたい．
|
| 次年度の研究費の使用計画 |
研究はほぼ順調に進展しているものの，他の利用可能な予算との関係で旅費等が次年度送りとなった．本年度は基礎検討が主であったが，次年度は開発の進展や成果発表が予想され，そのための旅費や人件費の支出が見込まれる．
|
