14:00 〜 14:20
[2E3-OS-13b-03] パラメタ付きモデルの到達可能性解析に基づくハイブリッドシステムモデリングツールの性能評価
キーワード：ハイブリッドシステム、到達可能性解析、パラメタ付きモデル
ハイブリッドシステムは, 時間の経過に伴ってシステムの変数が連続変化と離散変化を繰り返すシステムである. ハイブリッドシステムのモデリングを行うツールは数多く存在し, その一つとして上田らによるハイブリッドシステムモデリング言語HydLa およびその処理系 HyLaGI の開発が進んでいる.
HyLaGI は, 数式処理を用いたハイブリッドシステムの記号実行シミュレータであり, 初期状態にパラメータを扱えるという特徴を持つ. その他のモデリングツールとしては, 時間を細かく区切り数値計算により解軌道を凸集合で囲む SpaceEx や, 到達可能性問題とハイブリッドシステムを拡張して得られた SMT 問題を解いて到達可能性解析を行う dReach が挙げられるが, HyLaGI とこれらのツールの比較は十分に行われていない.
本研究は, 複数のハイブリッドシステムモデリングツールの比較および特性の考察を行うことを目的とする. 性能評価においては, パラメータを含む複数の例題による解析を行った.
HyLaGI は, 数式処理を用いたハイブリッドシステムの記号実行シミュレータであり, 初期状態にパラメータを扱えるという特徴を持つ. その他のモデリングツールとしては, 時間を細かく区切り数値計算により解軌道を凸集合で囲む SpaceEx や, 到達可能性問題とハイブリッドシステムを拡張して得られた SMT 問題を解いて到達可能性解析を行う dReach が挙げられるが, HyLaGI とこれらのツールの比較は十分に行われていない.
本研究は, 複数のハイブリッドシステムモデリングツールの比較および特性の考察を行うことを目的とする. 性能評価においては, パラメータを含む複数の例題による解析を行った.
講演PDFパスワード認証
論文PDFの閲覧にはログインが必要です。参加登録者の方は「参加者用ログイン」画面からログインしてください。あるいは論文PDF閲覧用のパスワードを以下にご入力ください。