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

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

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

反例ステートマシン図.png
やじるし.png
ステートマシン図に対応するコード.png