2015 Fiscal Year Annual Research Report
Deepening the implemenation technology of high-level modeling language implementations integrated with verifiers
| Project/Area Number |
26280024
|
|---|
| Research Institution | Waseda University |
|---|
Principal Investigator |
上田 和紀 早稲田大学, 理工学術院, 教授 (10257206)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
石井 大輔 福井大学, 工学(系)研究科(研究院), 講師 (00454025)
|
|---|
| Project Period (FY) |
2014-04-01 – 2017-03-31
|
| Keywords | 高水準モデリング言語 / 言語処理系 / モデル検査 / ハイブリッドシステム / 並列処理 |
|---|
| Outline of Annual Research Achievements |
ハイブリッドシステムモデリング言語HydLaの実行系HyLaGIおよびグラフ書換え言語LMNtalのモデル検査系SLIMの発展に向けて，以下の研究を実施した．
1. HydLaモデルの記号実行はモデルの挙動を正確に扱えるが数式の複雑化が問題となる．この解決には，計算時間と解の包囲性能において補完的な性質をもつ精度保証数値計算との統合が有効と考えられるが，後者が求める区間解は本来の解と定性的に異なる冗長領域を含む可能性がある．そこで，記号計算で得た情報を適切に利用することで冗長性を削減する方法を開発してHyLaGIに実装した．
2. HydLaモデルの検証技術について，実行が有限ステップで終わらないモデルの検証とモデルの進行性に関する検証の技法を定式化して試験実装した．また，微小時間に多数回の離散変化を起こすスライディングモードをもつモデルについて，微小量を記号的に表現することによってシミュレーションや解析を行う技法を提案した．
3. ハイブリッドシステムの解析や理解にはモデルの挙動の可視化が重要である．そこで，記号的に求解したHydLaモデルの軌道群を三次元空間上にプロットしてブラウズできるwebHydLaフロントエンドを開発し公開した．
4. グラフ書換え言語のグラフパターンの記述力の強化を目指して，再帰的定義が可能な文脈パターン機能とその効率的なマッチング方式を開発した．またそれらを実現した試験言語CSLMNtalの実行系を構築した．これによって，プログラミング言語の意味記述の道具であった文脈概念が，実際のプログラミング言語における強力な第一級言語機能として利用できることを示した．
5. モデル検査系SLIMはグラフを状態とする強力な状態空間構築・探索機能をもつ．その機能に拡張性をもたせて応用分野を拡大する第一歩として，LMNtalのためのメタプログラミング機能を設計し試験実装を行った．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
「研究実績の概要」に記載した各成果に加え，(i) グラフ書換え系モデル検査のための高効率状態表現技術に関する雑誌論文の採択と出版，(ii) 型なしラムダ計算をはじめとする形式的体系のLMNtalへの簡潔なエンコードを可能にする言語機能の提案，(iii) グラフの動的な型（再帰的文脈パターン）に加えて静的な型の検討の進捗，(iv) HydLaプログラムの静的解析に基づくデバッグ支援，をはじめとする多くの成果が得られた．また，LMNta言語の開発の動機となった並行論理型言語KL1の高効率並列処理系KLICの復活を行うなど，他の言語処理系との比較検討の素地も整えた．他方，これらの各要素技術の有効性をさらに多くの例題で確認し，実装技術を深めてメインストリームのモデリング言語処理系に統合することは今後の課題となっている．
|
| Strategy for Future Research Activity |
今年度は本基盤研究の最終年度にあたるため，実用規模の例題の記述実験や評価をさらに進めるとともに，有効性が明確となった要素技術のメインストリーム処理系（HyLaGIおよびSLIM）への統合を推進してゆき，HydLaおよびLMNtalのより高機能な処理系の整備と公開を行う．
多数の新たな要素技術のうち，メインストリーム処理系への統合には時期尚早と考えれるものについては，要素技術としての検討・試作・評価をさらに進めて次のステップの研究開発に結びつける．
|
| Causes of Carryover |
（研究代表者）海外研究出張旅費について，研究協力者の大学院生２名の旅費の一部を別予算から支出することとなったため．
（連携研究者）第１年度の残額分が持ち越されたため
|
| Expenditure Plan for Carryover Budget |
（研究代表者）サーバーマシンの増強費用に充てる予定である．
（研究分担者）出張旅費および消耗品に充てる予定である．
|
