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

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

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

     

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