Ansys SCADEは、作成したモデルに対して形式検証（SATソルバーを用いたモデル検査）を用いた検証が可能です。Ansys SCADEの形式検証は、作成したモデルに対して、想定される入力値であればいつでも所定の性質を満たすことを検査します。検査結果として性質を満たさない条件があれば、反例として入力値の組み合わせを変更します。この形式検証を用いることで、テストシナリオを複数作成せずとも検証を実施することが可能となります。
本事例では、反例を返すというモデル検査の特性を生かして、数独を説いてみました。モデル検査や数独に関しての具体的な紹介はこちらのブログ記事をご覧ください。