講演名 | 2019-03-14 SimulinkモデルのSMT-LIBエンコード方法に関する実験 武仲 紘輝(福井大), 石井 大輔(福井大), |
---|---|
PDFダウンロードページ | PDFダウンロードページへ |
抄録(和) | Simulink モデルの網羅テストなどにおいて,汎用プログラムと同様に SMT ソルバーを用いた静的解析が役立つ.そこで Simulink で作成した動的システムモデルを SMT-LIB 形式の記述へと変換する方法 (エンコード法) を検討する.変換結果を SMT ソルバーにより効率よく解析することを目標に,複数の変換方法を提案し,2つのSimulinkモデルを用いた実験により比較する. |
抄録(英) | Static analysis is useful for coverage testing etc. for Simulink models as for general-purpose programs. In this work, we consider encoding methods that translate a dynamical system model described with Simulink into an SMT-LIB description. Aiming at efficient static analysis with SMT solvers, we propose several encoding methods and evaluate them through experimenting with two Simulink models. |
キーワード(和) | MATLAB/Simulink / SMTソルバー / 静的解析 |
キーワード(英) | MATLAB/Simulink / SMT Solver / Static Analysis |
資料番号 | MSS2018-82 |
発行日 | 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モデルのSMT-LIBエンコード方法に関する実験 |
サブタイトル(和) | |
タイトル(英) | Experiment on SMT-LIB Encoding Methods for Simulink Models |
サブタイトル(和) | |
キーワード(1)(和/英) | MATLAB/Simulink / MATLAB/Simulink |
キーワード(2)(和/英) | SMTソルバー / SMT Solver |
キーワード(3)(和/英) | 静的解析 / Static Analysis |
第 1 著者 氏名(和/英) | 武仲 紘輝 / Koki Takenaka |
第 1 著者 所属(和/英) | 福井大学(略称:福井大) University of Fukui(略称:U. Fukui) |
第 2 著者 氏名(和/英) | 石井 大輔 / Daisuke Ishii |
第 2 著者 所属(和/英) | 福井大学(略称:福井大) University of Fukui(略称:U. Fukui) |
発表年月日 | 2019-03-14 |
資料番号 | MSS2018-82 |
巻番号(vol) | vol.118 |
号番号(no) | MSS-499 |
ページ範囲 | pp.7-11(MSS), |
ページ数 | 5 |
発行日 | 2019-03-07 (MSS) |