2023 Fiscal Year Annual Research Report
A Hybrid Model Checking Method for Model-Based Design of Embedded Systems
| Project/Area Number |
18K11234
|
|---|
| Research Institution | Ibaraki University |
|---|
Principal Investigator |
上田 賀一 茨城大学, 理工学研究科(工学野), 教授 (00213372)
|
|---|
| Project Period (FY) |
2018-04-01 – 2024-03-31
|
| Keywords | モデルベース開発 / モデル検証 / SMTソルバ / SysML |
|---|
| Outline of Annual Research Achievements |
本研究では，駆動型組込みシステムの実現において，制御ソフトの要求や制約をSysMLで表現する方法を規定，検査可能記述に変換しSMTソルバで解法する手順を開発することを具体的課題として取り組んできた．
まず，Z3Proverが非線形整数/実数演算と量化子を扱えることを確認し，SMTソルバの非線形性を扱える能力を試験的に実装した．その際，MATLAB/SimlinkとZ3Proverを連携させる評価において課題が残され，効率的な手法を探求してSMTソルバで制御ソフトの安定可能な解空間を得ること試みた．しかし，コロナ禍の影響で研究協力者が得られず，実プログラムの実装が進まず，確認できなかった．引き続き，研究協力者を募ったが，コロナ禍の影響で得られた協力時間が少なく，実装は部分的に留まった．一方で，非線形制御系の近似解法についても検討した．その後，MATLAB/SimlinkとSMTソルバの結合にあたり，SMT-LIB2.6のソルバ可換性に着目し，多くのSMTソルバに対応した協調解析ツールの開発を進めた．対象システムをSysMLモデル記述することで制約をモデル記述し，それをSMTソルバZ3の制約式に変換した上で，MATLAB/SimlinkとZ3を用いた協調解析手法を実装した．この際，Z3の量子化の適用事例として，モデルに配列構造を使用した記述が可能であることを示した．加えて，モデルの協調解析において記述能力の高いSMTソルバZ3Pyを選択し，汎用事例として4回転翼タイプのドローンを取り上げ，風などの外乱に対する推進力特性を解析および制約検証すべくハイブリッドモデルの構築に取り組んでいる．新たな研究協力者によりMATLAB/SimlinkとZ3Pyの協調解析手法の実装に当たっており，変更や調整が必要となるかもしれないが，継続すれば解析・検証手法として確立できるものと考えている．
|
