| 研究課題/領域番号 |
18K11234
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 基金 |
|---|
| 応募区分 | 一般 |
|---|
| 審査区分 |
小区分60050:ソフトウェア関連
|
|---|
| 研究機関 | 茨城大学 |
|---|
研究代表者 |
上田 賀一 茨城大学, 理工学研究科(工学野), 教授 (00213372)
|
|---|
| 研究期間 (年度) |
2018-04-01 – 2024-03-31
|
| 研究課題ステータス |
完了 (2023年度)
|
| 配分額 *注記 |
4,290千円 (直接経費: 3,300千円、間接経費: 990千円)
2020年度: 1,040千円 (直接経費: 800千円、間接経費: 240千円)
2019年度: 1,300千円 (直接経費: 1,000千円、間接経費: 300千円)
2018年度: 1,950千円 (直接経費: 1,500千円、間接経費: 450千円)
|
|---|
| キーワード | モデルベース開発 / 協調解析 / モデル検査 / ハイブリッド検証 / SMTソルバ / SysML / モデル検証 / 組込みシステム / ハイブリッドモデル |
|---|
| 研究成果の概要 |
組込みシステムのモデルベース設計のため，SysMLのブロック定義図，内部ブロック図，ブロックの内部構造，パラメトリック図により，対象システムの制御ソフトの要求や制約をモデル記述で表現した．このモデルをSimulinkとSMTソルバ上に記述展開したうえでハイブリッドモデル検査するにあたり，SMT-LIB2.6を用い，スクリプトのカスタマイズで，Simulinkと任意のSMTソルバを連動させたハイブリッド検証を可能とした．考案した制御ソフトの解空間獲得手法の処理手順を実装し，解空間を２次元マップにて可視化し，対話的に把握できることを事例ベースで確認した．
|
| 研究成果の学術的意義や社会的意義 |
組込みシステムの機能安全性を担保する手法として，制御モデルをシミュレーションで評価する方法が取られている．加えて，モデル検査を適用した検証を実現することで安全性を網羅的に担保できる．しかし，モデル検査手法は，モデル記述そのものが難しく，検証結果の把握や解釈も難しい．本研究では，SMTソルバで制御可能領域の解空間を探索する処理手順を実現し，開発現場で利用される実用的なモデルベース開発環境MATLAB/Simulink上で，従来の制御対象のプラントモデルのシミュレーションによる解析に，解空間の探索結果を反映し，影響を可視化し，把握や解釈を容易にすることを可能とした．
|
