top of page

  • モデル検査ツール（SPIN）実行機能は、検証用コードを使用してモデルの正しさを検証する機能

  • モデルが想定通りに構築できているか、前提となる仕様に不具合が含まれないかを検証する

  • それの出力は、なりたい状態へたどり着くルートを示す反例CSVファイル
    ⇒　検証結果として、目標状態に到達する１つのルートを示すファイルが出力
     

モデル検査を実施
（SPIN実行）
やじるし.png
ステートマシン図に対応するコード.png
検証結果.png
bottom of page