研究課題
制約概念に基づくハイブリッドシステムモデリング言語HydLaの実行系HyLaGIおよびグラフ書換え言語LMNtalのモデル検査系SLIMの発展に向けて，以下の研究を推進した。1. パラメタをもつモデルの記号実行を特徴とするHyLaGIに対して，精度保証数値計算の援用によって，記号求解ができない系を扱えるようにする拡張を実現した。離散変化条件の求解に焦点を当て，区間ニュートン法，アフィン演算，平均値定理を組み合わせることで，精度保証数値計算を援用しつつも記号パラメタに関する一次依存性を保存する技法を開発・実装し，例題を用いた評価を行った。2. ハイブリッドシステムの中には，スライディングモードをもつ系のように，相空間の狭い領域の中で多数回ないし無限回の離散変化を起こし，通常のシミュレーションが困難なものがある。そこで，記号実行によってパラメタをもつ系の繰返し的挙動を検出し，さらにループ不変条件を確認する技法を開発し，試験実装と評価を行った。3. LMNtalグラフを名前束縛を持つ形式的体系の記述に適用するための機能の設計と実装を行った。既存のhlgroundと呼ばれるハイパーグラフ型に対して，λ計算等に現れる代入操作を，複雑な付帯条件を記述しなくても変数捕捉なしに実現できるような拡張を行い，λ計算およびSystem F-subを例題とした記述実験と性能評価を行った。4. モデル検査器SLIMの機能拡張を容易にするために，LMNtal言語自身で非決定実行インタプリタやモデル検査器の実装を可能にするための第一級書換え規則と状態空間操作のためのAPIを設計実装し，それに基づいてCTLモデル検査器を含む新たなモデル検査器がLMNtalで記述できるようにした。5. 上記の諸成果をSLIMおよびHyLaGI処理系に反映させ，後者は新たにオープンソース化し，Githubから公開した。
28年度が最終年度であるため、記入しない。
すべて 2017 2016 その他
すべて 国際共同研究 (2件) 雑誌論文 (5件) (うち国際共著 1件、 査読あり 5件、 謝辞記載あり 4件、 オープンアクセス 1件) 学会発表 (17件) (うち国際学会 5件) 備考 (4件)
Proc. Sixth International Workshop on Design, Modeling, and Evaluation of Cyber Physical Systems, Lecture Notes in Computer Science
巻: 10107 ページ: 17-30
10.1007/978-3-319-51738-4_2
Science of Computer Programming
巻: 印刷中 ページ: 印刷中
Proc. 10th International Symposium on Theoretical Aspects of Software Engineering
巻: - ページ: 113-116
10.1109/TASE.2016.25
Proc. 23rd International Symposium on Temporal Representation and Reasoning
巻: - ページ: 4-11
10.1109/TIME.2016.8
Reliable Computing
巻: 23 ページ: 163-185
http://www.ueda.info.waseda.ac.jp/lmntal/
http://www.ueda.info.waseda.ac.jp/hydla/
https://github.com/lmntal
https://github.com/HydLa
