2020 Fiscal Year Annual Research Report
プログラミング言語技術との融合による高水準モデリング言語の進化と展開
| Project/Area Number |
18H03223
|
|---|
| Research Institution | Waseda University |
|---|
Principal Investigator |
上田 和紀 早稲田大学, 理工学術院, 教授 (10257206)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
石井 大輔 北陸先端科学技術大学院大学, 先端科学技術研究科, 准教授 (00454025)
|
|---|
| Project Period (FY) |
2018-04-01 – 2021-03-31
|
| Keywords | 高水準モデリング言語 / グラフ書換え / ハイブリッドシステム / 制約プログラミング / 発展可能処理系 |
|---|
| Outline of Annual Research Achievements |
プログラミング言語技術との融合による高水準モデリング言語とその処理系の進化を目標に，グラフ構造を扱うLMNtalおよび実数を扱うHydLaの二つのモデリング言語について以下の研究開発を実施した．
LMNtalについては以下の成果を得た：
(i) 今後の理論・実践研究の強固な基盤を与えるべく，LMNtalの構文と意味論を証明支援系Coq上で表現して，いくつかの重要な性質を証明した．(ii) データ構造をハイパーグラフに拡張したHyperLMNtalに対して構文主導の形式的意味論を整備して，HyperLMNtalに関する理論および処理系研究の基礎を与えた．(iii) 型の概念をもつワイルドカードをグラフパターンマッチングに活かすことで，ラムダ式の操作を含む応用を簡潔に記述する方法を開発し，公開中の処理系に組み込んだ．(iv) 形式文法の考え方に基づくグラフ型にIndex型の概念を導入し，グラフ書換えプログラムの型検査アルゴリズムの整備と改良を進め，実装と評価を通じて有効性を確認した．(v) グラフパターンマッチング機能の拡大を目指して，ユーザ定義の再帰的パターンを許す拡張言語CSLMNtalの実行アルゴリズムを整備改良し，既存のLMNtalコンパイラにその機能を組み込んだ．
制約に基づくハイブリッドシステムモデリング言語HydLaについては以下の成果を得た：
(i) 宣言的意味論の精査と精密化を行い，例題の形式的意味の証明支援系Coqによる検証を通じて意味論の妥当性を確認した．(ii) 時相論理式の記号実行という独自の特徴をもつHydLa処理系の検証能力をさらに高めるために，HydLaモデルからハイブリッドオートマトンへの変換アルゴリズムの改良と評価を進めた．
また，オープンソース公開しているLMNtalおよびHydLaの両処理系に対して，整備と改良のための集中作業を複数回実施した．
|
| Research Progress Status |
令和2年度が最終年度であるため、記入しない。
|
| Strategy for Future Research Activity |
令和2年度が最終年度であるため、記入しない。
|
Research Products
(20 results)
