組込みシステムのモデルベース設計のためのハイブリッドモデル検査手法の確立

2018 Fiscal Year Research-status Report

• Project/Area Number: 18K11234
• Research Institution: Ibaraki University
• Principal Investigator: 上田 賀一 茨城大学, 理工学研究科(工学野), 教授 (00213372)
• Project Period (FY): 2018-04-01 – 2021-03-31
• Keywords: モデルベース開発 / モデル検証 / SMTソルバ / SysML

Outline of Annual Research Achievements

産業界においては，駆動型組込みシステムの実現に苦慮している問題として，(１)制御対象のモデリング，(２)制御システム設計，(３)モデル検証，(４)モデルベース開発の統合開発環境が挙げられている．平成30年度は，問題(1)の解決に焦点を当てた研究に取り組み，ハイブリッドモデル検査のためのモデル表現方法を解決することを予定していた．具体的には，制御ソフトの要求や制約をSysMLで表現する方法を規定，検査可能記述に変換しSMT(Satis-fiable Modulo Theories，背景理論付き充足可能問題)ソルバで解法する手順を開発することである．まずは，SysMLでの表現については，ブロック定義図や内部ブロック図において制約記述部が大いに利用できることが想定でき，要素間関係の制約をパラメトリック図を用いて表現することが合理的であるとの考えに至った．制約記述をSMTソルバで検査可能な記述に変換するにあたり，線形性のみの制約ならば，SMTソルバでの解法においても線形式を扱えるだけで良い．しかし，非線形性を有する制約ではそうはいかないため，非線形性を扱えるSMTソルバについて調査することが必要となった．あらゆる非線形性制約を扱えるSMTソルバは確認できず，限定的ではあるが有用な非線形性を有するものとしてZ3Proverを確認できた．Z3Proverでは非線形整数/実数演算および量化子といった非線形性を扱うことができる．量化子を扱えることで一階述語論理の制約を記述できることは有用であり，SMTソルバにZ3Proverを選定し，限定的ではあるが非線形性を扱えるSMTソルバを対象に記述変換を試験的に実装した．

Current Status of Research Progress

3: Progress in research has been slightly delayed.

Reason

平成30年度は，問題(1)制御対象のモデリングの解決に焦点を当てた研究に取り組み，ハイブリッドモデル検査のためのSysMLによるモデル表現方法を解決することを予定していた．ハイブリッドモデル記述には，MATLAB／Limulinkで制御モデルを記述すること，SysMLで制約モデルを記述し，SMTソルバで検証可能な記述に変換することが含まれており，それぞれの記述が可能なことは今年度の検討により達成できたと考えている．しかし，制御モデルの記述において，非線形要素が加わった場合，記述はできても，SMTソルバによるモデル検査はできないことが予想された．そこで，サイドワークとして非線形制約を解法できるSMTソルバの調査検討が必要となり，取り組むこととしたため，当初計画で予定していなかった研究に取り組むこととなり，本来の問題に限れば，計画想定ほどの完成度を得ることができなかった．

Strategy for Future Research Activity

当初計画では，平成31年度はSMTソルバにより，制御ソフトの安定可能な解空間を得るための効率よい手法を検討し考案することとしていたが，非線形制約を扱う問題が生じたため，この問題を合理的に解決することを検討した上で，当初計画の研究に取り組むことを考える．現在，実用状況にあるSMTソルバの調査では，あらゆる非線形要素に対応できるものはないことが分かっている．そのため，実用上望ましいと考えられる非線形要素を選定し，対応可能なSMTソルバを用いることとした上で，制約記述中の非線形部分を前述の可能な非線形要素と従来の線形要素の合成で近似解法できるモデルへの変換手法を検討する．非線形制御をソフトウェア制御で実現する際には，非線形性をそのまま実現することはなく，同等のアルゴリズムや線形近似で実現することが一般的である．本研究においても，思考の類似性に基づいて，制約式の分割による部分非線形や線形近似のアプローチを取ることで問題は解決できるものと捉えている．

Causes of Carryover

物品価格等に多少の差額が生じたため，未使用額が生じた．次年度において消耗品等の購入に当てることとしたい．