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

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

基本信息

批准号：
18K11234
负责人：
上田賀一
金额：
$ 2.75万
依托单位：
Ibaraki University
依托单位国家：
日本
项目类别：
Grant-in-Aid for Scientific Research (C)
财政年份：
2018
资助国家：
日本
起止时间：
2018-04-01 至 2024-03-31
项目状态：
已结题

项目摘要

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

实现驱动嵌入式系统的挑战包括（1）受控对象的建模，（2）控制系统设计，（3）模型验证，以及（4）基于模型开发的集成开发环境。这项研究的具体任务是定义一种在 SysML 中表达控制软件需求和约束的方法，并开发一种将它们转换为可测试描述并使用 SMT 求解器求解的程序。在 2018 财年，我们确认 Z3Prover 可以处理非线性整数/实数运算和量词，尽管程度有限。我们通过实验实现了可以处理非线性的 SMT 求解器的描述性变换。然而，在控制模型中反映软件实现部分的评估以及将物理仿真应用于被控对象模型（MATLAB/Simlink和Z3Prover的协调）的问题仍然存在。 2019 年，我们研究了一种使用 SMT 求解器获得控制软件稳定解空间的有效方法来解决此问题。它使得从理论上处理量化成为可能，并导致对具有类似行为的并行运动控制系统进行简单模型描述（相当于数组描述）的可能性。我们无法确保研究合作者通过实施实际计划来确认该计划的实用性，因此我们无法实施或评估它。 2020财年和2023财年，我们计划寻找研究合作者并实施实施工作，但由于冠状病毒大流行的影响，我们的合作时间很短，实施仅限于链接MATLAB /的部分功能。 Simlink 和 Z3Prover ．作为非线性控制系统的近似求解方法，我们研究了通过级联部分线性近似来细化求解方法的思想。 2020财年，我们开发了一款专注于SMT-LIB2.6的协同分析工具，它兼容了很多SMT求解器，因为在模型协同中需要能够根据操作的特点和类型来选择SMT求解器分析。 ..但无法获得精通 MATLAB/Simlink 的研究合作者，且合作时间仅限于短时间内，且该方法只能应用于简单案例来确认实现，无法实现将其作为一种测试方法。