文献

J-GLOBAL ID：201902214765138548   整理番号：19A0889227

SimulinkモデルのSMT-LIBエンコード方法に関する実験

Experiment on SMT-LIB Encoding Methods for Simulink Models

著者 (2件)： 武仲紘輝 (福井大) ,  石井大輔 (福井大)
資料名： 電子情報通信学会技術研究報告  (IEICE Technical Report (Institute of Electronics, Information and Communication Engineers))
巻： 118  号： 499(MSS2018 81-95)  ページ： 7-11  発行年： 2019年03月07日 
JST資料番号： S0532B  ISSN： 0913-5685  資料種別： 会議録 (C)
記事区分： 原著論文  発行国： 日本 (JPN)  言語： 日本語 (JA)

抄録/ポイント： Simulinkモデルの網羅テストなどにおいて,汎用プログラムと同様にSMTソルバーを用いた静的解析が役立つ.そこでSimulinkで作成した動的システムモデルをSMT-LIB形式の記述へと変換する方法(エンコード法)を検討する.変換結果をSMTソルバーにより効率よく解析することを目標に,複数の変換方法を提案し,2つのSimulinkモデルを用いた実験により比較する.(著者抄録)

シソーラス用語： *シミュレータプログラム ,  計算機シミュレーション ,  *符号化 ,  組込みシステム ,  *システム設計 ,  応用プログラム ,  充足可能性問題
準シソーラス用語： *Simulink ,  *エンコード ,  ソルバ ,  充足問題

分類 (1件)： 計算機システム開発  (JD02010R)

引用文献 (5件)：

• R. Matinnejad, S. Nejati, L. C. Briand, and T. Bruckmann. SimCoTest: A Test Suite Generation Tool for Simulink/S-tateflow Controllers. ICSE, pages 585-588, 2016.
• S. Mohalik, A. Gadkari, Ambar, A. Yeolekar, K. C. Shashidhar, and S. Ramesh. Automatic test case generation from Simulink/Stateflow models using model checking. Software Testing, Verification and Reliability, 24: 155-180, 2014.
• M. Satpathy, A. Yeolekar, and S. Ramesh. Randomized Di-rected Testing (REDIRECT) for Simulink/Stateflow Mod-els. EMSOFT, pages 217-226, 2008.
• S. Sims and D. C. Duvarney. Experience Report: The Reactis Validation Tool. ICFP, pages 137-139, 2007.
• 冨田 尭,石井大輔,村上 徹,竹内成樹,青木利晃. 大規模複雑SimulinkモデルのためのMonte-Carlo最適化に基づいたテスト自動生成ツール. 組込みシステムシンポジウム, 2018.

タイトルに関連する用語 (5件)： Simulink ,  モデル ,  SMT ,  エンコード ,  実験