• モデル検査の結果として得られたファイル(反例CSVファイル)を可視化します。

  • 元のUML/SysMLモデル上に、変数の状態遷移の変化がアニメーション表示されます。

  • ユーザはテキストベースの結果ファイルを自力で解読することなく、アニメーションから直観的に不具合箇所を見つけ、UML/SysMLを修正することができます。

  • 上記の繰り返しで、不具合のないUML/SysMLモデルを作れます。