2022 Fiscal Year Research-status Report
組込みシステムのモデルベース設計のためのハイブリッドモデル検査手法の確立
| 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 |
駆動型組込みシステム実現の課題として，(1)制御対象のモデリング，(2)制御システム設計，(3)モデル検証，(4)モデルベース開発の統合開発環境が挙げられる．本研究では，制御ソフトの要求や制約をSysMLで表現する方法を規定，検査可能記述に変換しSMTソルバで解法する手順を開発することを具体的課題としている．
平成30年度に，限定的ではあるがZ3Proverにより非線形整数/実数演算と量化子を扱えることを確認した．非線形性を扱えるSMTソルバを対象に記述変換を試験的に実装した．しかし，ソフトウェア実現部分の評価を制御モデルに反映し物理シミュレーションをプラントモデルに適用する（MATLAB/SimlinkとZ3Proverの連携）課題は残った．
令和元年度は，この課題に対し，SMTソルバで制御ソフトの安定可能な解空間を得るための効率よい手法を検討した．量子化の理論的取り扱いを可能とし，同様の振舞いの並列動作制御系をシンプルにモデル記述（配列記述に相当）可能なことを導いた．実プログラムの実装による実用性の確認は，研究協力者を確保できず実装・評価に至らなかった．
令和2年度,3年度は，研究協力者を求め実装作業を予定したが，コロナ禍の影響で得られた協力時間はわずかで，実装はMATLAB/SimlinkとZ3Proverを連携させる部分機能に留まった．非線形制御系の近似解法として部分線形近似の連結による解法手法のアイデアの洗練を検討した．
令和4年度は，モデルの協調解析において演算や型の特性に応じてSMTソルバを選択できる必要があるため，多くのSMTソルバに対応したSMT-LIB2.6に着目した協調解析ツールを開発した．しかしMATLAB/Simlinkに長けた研究協力者が得られず，協力時間はわずかで実装確認の簡単な事例適用しかできず，検査手法としての確立には至らなかった．
|
| Current Status of Research Progress |
Current Status of Research Progress
4: Progress in research has been delayed.
Reason
本研究の目的は，制御対象のモデリングの適用可能性を検討するにあたり，一般性のあるアプローチへの対応を踏まえ，SMTソルバにより，制御ソフトの安定可能な解空間を得るための効率よい手法を検討し，考案することである．平成30年度の成果である量化子を扱えるZ3ProverをSMTソルバに選定することで一階述語論理の制約を記述できることをベースとし，同様の振舞いを並列動作する制御モデルに対し，シンプルなモデル記述（プログラミングで配列記述を利用できることに相当）が可能となることを令和元(平成31)年度に導いた．令和2年度・3年度は，研究遅れに対し，MATLAB/SimlinkとZ3Proverを連携させた実プログラムで実装し，この実用性を確認する予定であったが，コロナ禍により，プログラミング担当の研究協力者の確保はわずかな時間に限られ，連携させる部分機能の実現に留まった．研究代表者もコロナ禍等の学科運営の対応に時間を割かれ，本研究の時間確保が難しかった．令和4年度はモデルの協調解析において演算や型の特性に応じてSMTソルバを選択可能とするために，多くのSMTソルバに対応したSMT-LIB2.6に着目した協調解析ツールを開発したが，実装確認の簡単な事例適用しかできず，検査手法としての確立には至らなかった． そのため，協調解析ツールの実用性を評価できず，制御ソフトの安定可能な解空間を得るための効率よい手法の検討に入ることができなかった．
|
| Strategy for Future Research Activity |
令和4年度に残された課題，SMTソルバにより制御ソフトの安定可能な解空間を得るための効率よい手法の検討，および制御ソフトの解空間獲得手法とMatlab/Simulinkを連動させたハイブリッドモデル検査手法の確立に取り組む予定である．具体的には，Matlab/Simulinkとモデル検査の連携ソフトウェアの実装に向けた取り組みに合わせ，実用上望ましいと考えられる非線形要素に対し，適切なSMTソルバを用いて制約記述中の非線形部分を前述の可能な非線形要素と従来の線形要素の合成で近似解法できるモデルへの変換手法を検討する．非線形制御をソフトウェア制御で実現する際には，同等のアルゴリズムや線形近似で実現することが一般的であるので，本研究においても，思考の類似性に基づいて，制約式の分割による部分線形や線形近似のアプローチを取ることでモデル検査手法を確立したいと考えている．アイデアとして部分線形近似の連結による解法を適用できると考えており，技術者の経験知に基づく支援アプローチを踏まえてプログラム設計の検討を考えている．
|
| Causes of Carryover |
本研究では，ソフトウェアの試作にあたり，研究協力者として学生のアルバイトを予定していた．しかし，使用する開発環境のライセンスの都合から研究室にて取り組む必要があるため，コロナ禍が影響したこともあり，引き受けられる学生を必要な時間数で確保できず，次年度使用が生じた．次年度には，本作業の学生アルバイトを確保し進めたいと考える．また，使用する開発環境のライセンス契約の継続も必要となる．
|
