| 講演名 | 2019-03-15 Simulinkモデルに対するシミュレーションによる重み付き記号的状態遷移系の導出 大脇 亮太(名大), 結縁 祥治(名大), |
|---|---|
| PDFダウンロードページ |  PDFダウンロードページへ |
| 抄録(和) | 本研究では離散的な振舞いを含むSimulinkモデルの振る舞いを抽象化し記号的重み付き状態遷移系を導出する手法を提案する。連続的な変数の値を固定した区間から構成される領域で分割し、連続的な振る舞いを抽象化することで遷移系を生成する。サンプリング時間ごとの連続変数の変化を領域の端点におけるシミュレーションを元にして、重みづけを遷移に対して与える。遷移の重みづけの積として遷移系上のトレースに対して重要度を定める。遷移系の振舞いの性質をチェックすることで、Simulinkモデルの振舞いに対して既存のモデル検査が適用できるようになり、振舞いの概要が機械的にチェックできるようになることが期待できる。本稿ではオートマティックトランスミッションに対して適用し記号的重み付き遷移系を導出した例を示す。 |
| 抄録(英) | We propose a method to generate a symbolic weighted transition systemfrom a Simulink model description. Continuous values for variablesare abstracted by fixed intervals to form regions. Value changes withtime passage are translated as the transitions over regions accordingto the fixed sampling time. We compute the next regions by simulationof the given model. Assuming the system behavior is monotonic at allinstants, we calculate the next possible region from the simulation ofedge points. We expect the transition systems generated hold thepreserves behavior of the given Simulink model and enables to applythe existing testing methods such as the model checking. Weillustrate our approach by deriving the symbolic transition system forthe automatic transition system available as an example of Simulink. |
| キーワード(和) | Simulink / モデル検査 / 重み付き状態遷移系 / シミュレーション |
| キーワード(英) | Simulink / Model Checking / Weighted Transition System / Simulation |
| 資料番号 | MSS2018-95 |
| 発行日 | 2019-03-07 (MSS) |
| 研究会情報 | |
| 研究会 | NLP / MSS |
|---|---|
| 開催期間 | 2019/3/14(から2日開催) |
| 開催地（和） | 福井大学 文京キャンパス |
| 開催地（英） | Bunkyo Camp., Univ. of Fukui |
| テーマ（和） | SICE-DES研究会，IEICE-MSS研究会，IEICE-NLP研究会の3研究会併催，一般およびWork In Progress(WIP) |
| テーマ（英） | SICE-DES, IEICE-MSS, IEICE-NLP, Work In Progress, and etc. |
| 委員長氏名（和） | 高橋 規一(岡山大) / 名嘉村 盛和(琉球大) |
| 委員長氏名（英） | Norikazu Takahashi(Okayama Univ.) / Morikazu Nakamura(Univ. of Ryukyus) |
| 副委員長氏名（和） | 黒川 弘章(東京工科大) / 髙井 重昌(阪大) |
| 副委員長氏名（英） | Hiroaki Kurokawa(Tokyo Univ. of Tech.) / Shigemasa Takai(Osaka Univ.) |
| 幹事氏名（和） | 山内 将行(広島工大) / 木村 貴幸(日本工大) / 豊嶋 伊知郎(東芝エネルギーシステムズ) / 金澤 尚史(阪大) |
| 幹事氏名（英） | Masayuki Yamauchi(Hiroshima Inst. of Tech.) / Takayuki Kimura(Nippon Inst. of Tech.) / Ichiro Toyoshima(Toshiba) / Takahumi Kanazawa(Osaka Univ.) |
| 幹事補佐氏名（和） | 木村 真之(京大) / 島田 裕(埼玉大) / 金城 秀樹(沖縄大) |
| 幹事補佐氏名（英） | Masayuki Kimura(Kyoto Univ.) / Yutaka Shimada(Saitama Univ.) / Hideki Kinjo(Okinawa Univ.) |
| 講演論文情報詳細 | |
| 申込み研究会 | Technical Committee on Nonlinear Problems / Technical Committee on Mathematical Systems Science and its applications |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | Simulinkモデルに対するシミュレーションによる重み付き記号的状態遷移系の導出 |
| サブタイトル（和） | |
| タイトル（英） | A derivation of weighted transition system for Simulink models from simulation results |
| サブタイトル（和） | |
| キーワード(1)（和/英） | Simulink / Simulink |
| キーワード(2)（和/英） | モデル検査 / Model Checking |
| キーワード(3)（和/英） | 重み付き状態遷移系 / Weighted Transition System |
| キーワード(4)（和/英） | シミュレーション / Simulation |
| 第 1 著者 氏名（和/英） | 大脇 亮太 / Ryota Owaki |
| 第 1 著者 所属（和/英） | 名古屋大学(略称：名大) Nagoya University(略称：Nagoya Univ) |
| 第 2 著者 氏名（和/英） | 結縁 祥治 / Shoji Yuen |
| 第 2 著者 所属（和/英） | 名古屋大学(略称：名大) Nagoya University(略称：Nagooya Univ) |
| 発表年月日 | 2019-03-15 |
| 資料番号 | MSS2018-95 |
| 巻番号（vol） | vol.118 |
| 号番号（no） | MSS-499 |
| ページ範囲 | pp.75-80(MSS), |
| ページ数 | 6 |
| 発行日 | 2019-03-07 (MSS) |