2013 Fiscal Year Annual Research Report
高性能検証系を統合した高水準モデリング言語処理系の構築
| Project/Area Number |
23300011
|
|---|
| Research Institution | Waseda University |
|---|
Principal Investigator |
上田 和紀 早稲田大学, 理工学術院, 教授 (10257206)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
田辺 良則 国立情報学研究所, 大学共同利用機関等の部局等, 教授 (60443199)
|
|---|
| Project Period (FY) |
2011-04-01 – 2014-03-31
|
| Keywords | 高水準モデリング言語 / 言語処理系 / モデル検査 / ハイブリッドシステム / 並列処理 |
|---|
| Research Abstract |
実行系と検証系を統合した高水準モデリング言語の構築に関して，以下の二つの処理系を軸に研究開発を実施した．
1. ハイブリッドシステムモデリング言語HydLaの記号実行シミュレータHyroseについて以下の開発を進めた．(a) 無限時間モデル検査への発展を視野に入れて，前年度検討したHydLaからハイブリッドオートマトンへの変換技法を改良して実装した．(b) 記号的に解けない問題の解の存在範囲を正しく計算するために，記号実行処理系にアフィン演算を統合的に導入する方法の基礎検討を行った．(c) 制約が矛盾する原因をunsat coreを用いて説明するための機能をインタラクティブ実行系に組み込んだ．(d) Hyroseの基本演算である制約求解について，求解結果の再利用や制約間の依存関係解析に基づく最適化アルゴリズムを開発し実装を行った．(e) 求解エンジンとしてMathematicaに加えてREDUCEを使えるように拡張を行った．
2. 階層グラフ書換えに基づくモデリング言語LMNtalとその処理系について以下の研究開発を進めた．(a) 並列モデル検査機能について，MAPとNested DFSの複合によって効率とスケーラビリティを改善する方法を実装し評価を行った．(b) モデル検査における状態空間構築で重要な多数のグラフ構造間の同型性判定を効率化するために，グラフ間の差分情報に着目してグラフ正規化のコストを削減する手法を開発して試験実装と評価を行った．(c) 大規模グラフ書換えの並列処理を可能にする抽象機械命令を導入して評価を行った．(d) ハイパーグラフ書換え系への拡張について，多相型推論や論理型言語の実装実験を通じて有効性評価と処理系の保守改良を進めた．(e) LMNtalの文脈機能の拡張に向けて，ユーザ定義文脈機能の試験実装および例題記述実験を行った．(f) 汎用性の高い新たな実行可視化環境Grapheneの設計と実装を行った．
|
| Current Status of Research Progress |
Reason
25年度が最終年度であるため、記入しない。
|
| Strategy for Future Research Activity |
25年度が最終年度であるため、記入しない。
|
