Simulinkモデルに対するシミュレーションによる重み付き記号的状態遷移系の導出

摘要

本研究では離散的な振舞いを含むSimulinkモデルの振る舞いを抽象化し記号的重み付き状態遷移系を導出する手法を提案する。連続的な変数の値を固定した区間から構成される領域で分割し、連続的な振る舞いを抽象化することで遷移系を生成する。サンプリング時間ごとの連続変数の変化を領域の端点におけるシミュレーションを元にして、重みづけを遷移に対して与える。遷移の重みづけの積として遷移系上のトレースに対して重要度を定める。遷移系の振舞いの性質をチェックすることで、Simulinkモデルの振舞いに対して既存のモデル検査が適用できるようになり、振舞いの概要が機械的にチェックできるようになることが期待できる。本稿ではオートマティックトランスミッションに対して適用し記号的重み付き遷移系を導出した例を示す。