| Project/Area Number |
18K11234
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Multi-year Fund |
|---|
| Section | 一般 |
|---|
| Review Section |
Basic Section 60050:Software-related
|
|---|
| Research Institution | Ibaraki University |
|---|
Principal Investigator |
Ueda Yoshikazu 茨城大学, 理工学研究科(工学野), 教授 (00213372)
|
|---|
| Project Period (FY) |
2018-04-01 – 2024-03-31
|
| Project Status |
Completed (Fiscal Year 2023)
|
| Budget Amount *help |
¥4,290,000 (Direct Cost: ¥3,300,000、Indirect Cost: ¥990,000)
Fiscal Year 2020: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000)
Fiscal Year 2019: ¥1,300,000 (Direct Cost: ¥1,000,000、Indirect Cost: ¥300,000)
Fiscal Year 2018: ¥1,950,000 (Direct Cost: ¥1,500,000、Indirect Cost: ¥450,000)
|
|---|
| Keywords | モデルベース開発 / 協調解析 / モデル検査 / ハイブリッド検証 / SMTソルバ / SysML / モデル検証 / 組込みシステム / ハイブリッドモデル |
|---|
| Outline of Final Research Achievements |
Using SysML, the requirements and constraints of the control software of the target system are expressed in a model description. The model is deployed on Simulink and SMT solvers, and SMT-LIB 2.6 is used to enable hybrid verification by linking Simulink and an arbitrary SMT solver. We implemented the procedure of the solution space acquisition method for control software, and confirmed its usefulness on a case study basis.
As a method to guarantee functional safety of embedded systems, in addition to evaluating control models by simulation, safety can be comprehensively guaranteed by realizing verification by applying model checking. However, model checking methods are also difficult to describe models and to interpret verification results. Our method reflects the results of model verification by constraints in the simulation-based evaluation of plant models used at development sites, making it possible to visualize the effects and facilitating understanding and interpretation.
|
| Academic Significance and Societal Importance of the Research Achievements |
組込みシステムの機能安全性を担保する手法として，制御モデルをシミュレーションで評価する方法が取られている．加えて，モデル検査を適用した検証を実現することで安全性を網羅的に担保できる．しかし，モデル検査手法は，モデル記述そのものが難しく，検証結果の把握や解釈も難しい．本研究では，SMTソルバで制御可能領域の解空間を探索する処理手順を実現し，開発現場で利用される実用的なモデルベース開発環境MATLAB/Simulink上で，従来の制御対象のプラントモデルのシミュレーションによる解析に，解空間の探索結果を反映し，影響を可視化し，把握や解釈を容易にすることを可能とした．
|
