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

嵌入式系统模型设计混合模型检验方法的建立

• 批准号: 18K11234
• 负责人: 上田 賀一
• 金额: $ 2.75万
• 依托单位: Ibaraki University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research (C)
• 财政年份: 2018
• 资助国家: 日本
• 起止时间: 2018-04-01 至 2024-03-31
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/en/grant/KAKENHI-PROJECT-18K11234/
• 关键词: モデルベース開発; モデル検証; SMTソルバ; SysML; 組込みシステム; ハイブリッドモデル

駆動型組込みシステム実現の課題として，(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に長けた研究協力者が得られず，協力時間はわずかで実装確認の簡単な事例適用しかできず，検査手法としての確立には至らなかった．

The problems of dynamic system development are as follows: (1) control object design,(2) control system design,(3) control object identification,(4) control object development and integrated development environment. This study aims to define the requirements of the SMT solution and the methods to control SysML performance, and to examine the possible development of the SMT solution. Heisei 30 years ago, the limit of Non-linear SMT solution for image description of the change in the test results. In this paper, the author discusses the problem of how to evaluate the performance of software and how to control the performance of software and how to reflect the performance of software and hardware. In order to solve this problem, SMT should be able to control the stability of the system. The theory of quantization can be used to describe the parallel motion control system in the same way. To confirm the usefulness of the equipment, research collaborators should ensure that the equipment can be evaluated. In 2002 and 2003, the research collaborator requested the implementation of the installation work, and the impact of the disaster was obtained. The cooperation time was changed. The implementation of the MATLAB/Simlink and Z3Prover was connected to some functions. The approximate solution of non-linear shape control system and the link of partial linear shape approximation are discussed. In 2005 and 2004, the SMT-LIB 2.6 was launched for the coordination analysis of SMT-LIB 2.6. MATLAB/Simlink research collaborators have been working together for a long time. Collaboration time has been working together to confirm simple case applications. Inspection methods have been established.

项目成果

SimulinkとSMTソルバの連携による協調解析支援ツールの開発

通过链接 Simulink 和 SMT 求解器开发协同分析支持工具

• 发表时间: 2023
• 作者: Ryo Kurachi;Hiroaki Takada;Naoki Adachi;Hiroshi Ueda;Yukihiro Miyashita;Engielista Anak Norman，上田賀一
• 通讯作者: Engielista Anak Norman，上田賀一