| 電子情報通信学会 研究会発表申込システム 講演論文 詳細 |
技報閲覧サービス [ログイン] 技報アーカイブ |
| トップに戻る | 前のページに戻る | [Japanese] / [English] |
| 講演抄録／キーワード | ||
| 講演名 | 2025-03-22 13:10 ドローンモデルを事例とした協調解析による不具合検出 ○阿部慎太郎・上田賀一（茨城大）  KBSE2024-63 |
|
| 抄録 | （和） | 組込みシステムの検査手法として，形式検証とシミュレーションを組み合わせた協調解析という手法が研究されている．先行研究では， Simulink と Yices を用いた組込みシステムにおける充足可能性の検査手法が提案されている．しかし，SMT ソルバ Yices は小規模問題に適し，効率的なアルゴリズムで解法するという特徴を持つことから学術的研究では有用なものの，より汎用的な解析に向いた SMT ソルバとは言えない．本研究では，産業界の利用が広範でより大規模問題にも対応可能なSMT ソルバ Z3 の利用を考え，Simulink と Python インタフェース利用の Z3py を用いた協調解析による不具合検出手法を提案する．本手法はより広範な協調解析を可能とし，解析対象を拡張できると考える．本手法の妥当性評価として，ドローンモデルを対象とした評価実験を行い，突風により発生するドローンモデルの不具合検出を事例として紹介する． |
| （英） | Co-analysis, a method that combines formal verification and simulation, is researched as a verification method for embedded systems. Previous research has proposed a method for testing satisfiability using Simulink and Yices. The SMT solver Yices is useful in academic research because it is suitable for small-scale problems and uses efficient algorithms to solve them. However, this SMT solver is not suitable for more general-purpose analysis. In this study, we therefore consider using the SMT solver Z3, which is widely used in industry and can handle large-scale problems, and propose a method for detecting defects through co-analysis using Simulink and Z3py. This method enables a wider range of co-analysis and can expand the scope of analysis. In this report, we conduct evaluation experiments using a drone model to evaluate the validity of this method, and explain the detection of defects in a drone model caused by gusts of wind as an example. | |
| キーワード | （和） | 協調解析 / Simulink / Z3py / 組込みシステム / / / / |
| （英） | Co-Analysis / Simulink / Z3py / Embedded System / / / / | |
| 文献情報 | 信学技報, vol. 124, no. 449, KBSE2024-63, pp. 65-70, 2025年3月. | |
| 資料番号 | KBSE2024-63 | |
| 発行日 | 2025-03-14 (KBSE) | |
| ISSN | Online edition: ISSN 2432-6380 | |
| 著作権に ついて |
技術研究報告に掲載された論文の著作権は電子情報通信学会に帰属します．(許諾番号：10GA0019/12GB0052/13GB0056/17GB0034/18GB0034) | |
| PDFダウンロード | KBSE2024-63 |
|
| 研究会情報 | |
| 研究会 | KBSE |
| 開催期間 | 2025-03-21 - 2025-03-22 |
| 開催地（和） | B-nest 静岡市産学交流センター |
| 開催地（英） | |
| テーマ（和） | 一般 |
| テーマ（英） | |
| 講演論文情報の詳細 | |
| 申込み研究会 | KBSE |
| 会議コード | 2025-03-KBSE |
| 本文の言語 | 日本語 |
| タイトル（和） | ドローンモデルを事例とした協調解析による不具合検出 |
| サブタイトル（和） | |
| タイトル（英） | Defect detection through co-analysis using a drone model |
| サブタイトル（英） | |
| キーワード(1)（和/英） | 協調解析 / Co-Analysis |
| キーワード(2)（和/英） | Simulink / Simulink |
| キーワード(3)（和/英） | Z3py / Z3py |
| キーワード(4)（和/英） | 組込みシステム / Embedded System |
| キーワード(5)（和/英） | / |
| キーワード(6)（和/英） | / |
| キーワード(7)（和/英） | / |
| キーワード(8)（和/英） | / |
| 第1著者 氏名（和/英/ヨミ） | 阿部 慎太郎 / Shintaro Abe / アベ シンタロウ |
| 第1著者 所属（和/英） | 茨城大学 (略称： 茨城大) Ibaraki University (略称： Ibaraki Univ.) |
| 第2著者 氏名（和/英/ヨミ） | 上田 賀一 / Yoshikazu Ueda / ウエダ ヨシカズ |
| 第2著者 所属（和/英） | 茨城大学 (略称： 茨城大) Ibaraki University (略称： Ibaraki Univ.) |
| 講演者 | 第1著者 |
| 発表日時 | 2025-03-22 13:10:00 |
| 発表時間 | 30分 |
| 申込先研究会 | KBSE |
| 資料番号 | KBSE2024-63 |
| 巻番号（vol） | vol.124 |
| 号番号（no） | no.449 |
| ページ範囲 | pp.65-70 |
| ページ数 | 6 |
| 発行日 | 2025-03-14 (KBSE) |
[研究会発表申込システムのトップページに戻る]