組込みシステムのソフトウェアモデルとコードが正しく動作することを確認する際に,形式検証/形式手法が役立ちます。設計エラーを検出するために,形式検証/形式手法は数学的に厳密な手順を活用し,モデルやコードベースのすべての可能な実行パスを検索します。モデルやモデルから生成されたコードに対する形式検証/形式手法が可能です。
モデルの形式検証/形式手法
モデルに形式検証/形式手法を採用することにより,モデル内のエラーを検出し,シミュレーションでエラーを再現するテストベクトルを生成することができます。期待される結果が具体的なデータで表現されている従来の試験方法と異なり,形式検証/形式手法は,システムの動作を表すモデルを用いて実行できます。このようなモデルは,テストシナリオや期待する/期待しないシステム動作を検証目的として含めることができます。このようなモデルを用いて行った形式検証/形式手法は,シミュレーションを補完し,ユーザの設計をより深く理解することが出来ます。
詳細については,金宝app仿真软件设计校验™を参照してください。
コードの形式検証/形式手法
静的コード解析や形式検証/形式手法を使用することにより,ツールを用いてC / c++またはAdaソースコード内にオーバーフローやゼロ除算,範囲外の配列へのアクセス,その他の特定のランタイムエラーの検出,または存在しないことを証明できます。これらのツールを用いて,手書きまたは生成された組込みソフトウェアのコード検証を行うことができます。また,コーディング規格への準拠やコード複雑度メトリックスの確認とソフトウェアの品質を測定できます。
詳細については,Polyspace®を参照してください。
