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

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

基本信息

批准号：
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年和2020财政年度，我们计划在2020年和2020年实施该项目，但是由于Covid-19的大流行的影响，合作时间仅少量，并且该实施仅限于链接Matlab/SimLink和Z3Prover的部分功能。我们使用部分线性近似作为非线性控制系统的近似解决方案来研究解决方案方法的思想。在2022年，由于有必要根据计算的特征和模型协作分析中的特征选择SMT求解器，因此我们开发了一个集中在SMT-LIB2.6上的协作分析工具，该工具支持许多SMT求解器。但是，没有任何在MATLAB/SIMLINK上熟练的研究合作者，并且合作时间是有限的，并且可以在简单的情况下应用实施确认，从而无法建立检查方法。

项目成果

期刊论文数量（1）

专著数量（0）

科研奖励数量（0）

会议论文数量（0）

专利数量（0）

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

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

DOI：
发表时间：
2023
期刊：
影响因子：
0
作者：
Ryo Kurachi;Hiroaki Takada;Naoki Adachi;Hiroshi Ueda;Yukihiro Miyashita;Engielista Anak Norman，上田賀一
通讯作者：
Engielista Anak Norman，上田賀一