top of page
モデル検査

  • ある現象について、確率は低くても理論的に起きる可能性があるかどうかを検出する手法です。

  • シミュレーションが、人の手でシナリオを作成するのに対し、モデル検査では自動的にシナリオを作成し網羅的な検査を行うことができます。

  • 出現率が低くシミュレーションだけでは検出の難しい「望ましくない状態」への遷移が起こり得るかどうかを検出するのに適しています

SPIN

  • SPINはモデル検査のツールです。

  • SPINによるモデル検査により、以下の検証が可能です

    • UMLSysMLのモデル図が正しく構築できているか、不整合はないか

    • モデル図の基となる仕様に誤りがないか

  • SPINによるモデル検査を実行するには、対象となるモデル図から専用の検証用コード（Promelaコード）を作成し、SPINに入力する必要があります

bottom of page