组込みシステムのソフトウェアモデルとコードが正しく动作することを确认する际に，形式検证/形式手法が役立ちます。设计エラーを検出するために，形式検证/形式手法は数学的に厳密な手顺を活用し，モデルやコードベースのすべての可能な実行パスを検索します。モデルやモデルから生成されたコードに対する形式検证/形式手法が可能です。

モデルの形式検证/形式手法

モデルに形式検证/形式手法を采用することにより，モデル内のエラーを検出し，シミュレーションでエラーを再现するテストベクトルを生成することができます。期待される结果が具体的なデータで表现されている従来の试験方法と异なり，形式検证/形式手法は，システムの动作を表すモデルを用いて実行できます。このようなモデルは，テストシナリオや期待する/期待しないシステム动作を検证目的として含めることができます。このようなモデルを用いて行った形式検证/形式手法は，シミュレーションを补完し，ユーザの设计をより深く理解することが出来ます。

详细については，万博1manbetxSimulink设计验证器™を参照してください。

コードの形式検证/形式手法

静的コード解析や形式検证/形式手法を使用することにより，ツールを用いてC / C ++または阿达ソースコード内にオーバーフローやゼロ除算，范囲外の配列へのアクセス，その他の特定のランタイムエラーの検出，または存在しないことを证明できます。これらのツールを用いて，手书きまたは生成された组込みソフトウェアのコード検证を行うことができます。また，コーディング规格への准拠やコード复雑度メトリックスの确认とソフトウェアの品质を测定できます。

详细については，Polyspace^®を参照してください。