弊社社員が共著で論文を発表しました

弊社開発3部　髙井が共著で論文を発表しました。

組込みシステムの開発には、MATLAB/Simulinkで記述されるようなモデルの形式的な解析が必要されています。
しかしながら、産業用モデルの複雑化に伴い、解析が困難になっています。

本論文では、SMTソルバを用いたSimulinkモデルのモデル検査手法を提案します。

本手法は、以下を目的に提案します。
（1）複雑なモデルの自動的、効率的、かつ理解しやすい検証
（2）モデルの数値的に精確な解析
（3）SMTソルバ（ここでは Z3）を用いた Simulinkモデルの解析デモ

具体的には、最初に対象となるモデルを、算術演算とビットベクトルの領域で述語論理式に符号化を行います。
次に様々なSimulinkブロックを正確に符号化する方法を探ります。
そして、対象ブロックが関与するサブシステムを抽出し、
実行経路をインクリメンタルに展開するK帰納法(K-induction)をベースとするアルゴリズムを用い、与えられた不変性プロパティを検証する、という一連の手法となります。

（検証）実験では、提案手法と他のツールを一連のモデルや性質へ適用しました。
結果、本論での提案手法が、他ツールで検証できない特性を含む、ほとんどの特性で適用可能なことを検証できました。



https://arxiv.org/abs/2206.02992