​モデルベース形式検証ツール

ユーザが作成したUML/SysMLのモデル図から、検証用コード(Promelaコード)を自動生成する機能です。

Promelaコードは、モデル検査ツール（SPIN）を実行するための特殊なコードです。この機能により生成されるコードが、②SPIN実行機能の入力となります。

モデル図から検証用コードを自動で生成できるため、設計者がモデルから自力でコーディングをする必要がありません。