2018 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について，以下の新言語機能の設計と実装を行った。(1)全称量化子を伴うグラフパターンマッチングの意味論を定め，仮想機械での実装を実現し例題記述を行った。(2)λ計算の簡約を簡潔に記述するための新たなグラフ型を提案し実装した。(3)モデル検査における並行プロセスの自動抽象化技法能を提案し，正当性を証明し実装を行った。また正当性証明のためにLMNtalの操作的意味論の検討と整備を行った。(4)LMNtalグラフの既存の型概念を検討して再定式化を行った。(5)グラフのための内包表記の検討を進めた。(6)非決定実行インタプリタの記述を可能にするAPIを定めて公開した。
LMNtal実行・検証系については，集中作業合宿を実施してC++化による可読性・保守性の改善作業を行うとともに，LMNtalモデル検査器の要素技術となるグラフ差分を利用した効率的グラフ正規化技法の処理系への組み込みを進めた。
制約概念に基づくハイブリッドシステムモデリング言語HydLaについては，言語機能と実装技法について以下の研究開発を行った。(1)変数および制約階層の動的生成のための記法を定めて実装を行った。(2)シミュレーション中の制約処理過程を動的に解析して再利用する技法の開発を行った。(3)モデル抽象化技法を実行性能改善に応用する技法を開拓した。(4)記号パラメタをもつ非線形常微分方程式の精度保証近似解法の開発と評価を行った。(5)微分代数方程式の求解性能向上方法の検討を進めた。(6)集中検討合宿を行って，オープンソース制約エンジンの有力候補となるSageMathの評価検討を行った。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
研究開発のコアとなる二つのモデリング言語の言語機能と実装技法について，多岐にわたる要素技術の開拓を進めることができた。これには，年度末時点では設計の詰めの段階で初回の学会発表を行ったばかりのものも一部含まれるが，多くは試験実装を経て評価・改良中，またはGithubで公開中の処理系の主たるブランチにすでに反映済みである。
研究分担者および連携研究者との交流も進め，フランス・ナント大学の制約プログラミング研究グループとも相互訪問を行った。
|
| Strategy for Future Research Activity |
プログラミングおよびモデリング言語の研究開発における理論と実践の強い連携という基本方針に基づいて，育ってきた要素技術を発展させてGithubから公開中のモデリング言語実行・検証系に統合する作業を推進する。
LMNtalとその処理系については，(1)言語機能としてほぼ確立できた高階概念の本格実装および応用の展開，(2)グラフのための強力な型体系の，グラフの型検査からグラフ書換え規則の型検査への発展，(3)全称量化グラフパターンにマッチしたグラフの書き換えのための構文，意味論，実装の整備，などを進める。
HydLaとその処理系については，特に(1)処理系の基礎をなす操作的意味論と言語仕様の根幹をなす宣言的意味論の整合性の検討，(2)プログラムの等価性のより深い検討およびそれを支える精密な意味論の整備，(3)プログラム変換技法の開発とその実行最適化への応用，(4)制約エンジンの求解能力および性能向上，などを進める。
|
