2016 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. パラメタをもつモデルの記号実行を特徴とするHyLaGIに対して，精度保証数値計算の援用によって，記号求解ができない系を扱えるようにする拡張を実現した。離散変化条件の求解に焦点を当て，区間ニュートン法，アフィン演算，平均値定理を組み合わせることで，精度保証数値計算を援用しつつも記号パラメタに関する一次依存性を保存する技法を開発・実装し，例題を用いた評価を行った。
2. ハイブリッドシステムの中には，スライディングモードをもつ系のように，相空間の狭い領域の中で多数回ないし無限回の離散変化を起こし，通常のシミュレーションが困難なものがある。そこで，記号実行によってパラメタをもつ系の繰返し的挙動を検出し，さらにループ不変条件を確認する技法を開発し，試験実装と評価を行った。
3. LMNtalグラフを名前束縛を持つ形式的体系の記述に適用するための機能の設計と実装を行った。既存のhlgroundと呼ばれるハイパーグラフ型に対して，λ計算等に現れる代入操作を，複雑な付帯条件を記述しなくても変数捕捉なしに実現できるような拡張を行い，λ計算およびSystem F-subを例題とした記述実験と性能評価を行った。
4. モデル検査器SLIMの機能拡張を容易にするために，LMNtal言語自身で非決定実行インタプリタやモデル検査器の実装を可能にするための第一級書換え規則と状態空間操作のためのAPIを設計実装し，それに基づいてCTLモデル検査器を含む新たなモデル検査器がLMNtalで記述できるようにした。
5. 上記の諸成果をSLIMおよびHyLaGI処理系に反映させ，後者は新たにオープンソース化し，Githubから公開した。
|
| Research Progress Status |
28年度が最終年度であるため、記入しない。
|
| Strategy for Future Research Activity |
28年度が最終年度であるため、記入しない。
|
| Causes of Carryover |
28年度が最終年度であるため、記入しない。
|
| Expenditure Plan for Carryover Budget |
28年度が最終年度であるため、記入しない。
|
