形式的検証

形式的検証とは?

組込みシステムのソフトウェアモデルとコードが正しく動作することを確認する際に、形式検証/形式手法が役立ちます。設計エラーを検出するために、形式検証/形式手法は数学的に厳密な手順を活用し、モデルやコードベースのすべての可能な実行パスを検索します。モデルやモデルから生成されたコードに対する形式検証/形式手法が可能です。

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

モデルに形式検証/形式手法を採用することにより、モデル内のエラーを検出し、シミュレーションでエラーを再現するテストベクトルを生成することができます。期待される結果が具体的なデータで表現されている従来の試験方法と異なり、形式検証/形式手法は、システムの動作を表すモデルを用いて実行できます。このようなモデルは、テストシナリオや期待する/期待しないシステム動作を検証目的として含めることができます。このようなモデルを用いて行った形式検証/形式手法は、シミュレーションを補完し、ユーザの設計をより深く理解することが出来ます。

詳細については、Simulink Design Verifier™を参照してください。

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

静的コード解析や形式検証/形式手法を使用することにより、ツールを用いてC/C++またはAdaソースコード内にオーバーフローやゼロ除算、範囲外の配列へのアクセス、その他の特定のランタイムエラーの検出、または存在しないことを証明できます。これらのツールを用いて、手書きまたは生成された組込みソフトウェアのコード検証を行うことができます。また、コーディング規格への準拠やコード複雑度メトリックスの確認とソフトウェアの品質を測定できます。

詳細については、Polyspace®を参照してください。


製品使用例および使い方

参考: 静的コード解析, Simulink Design Verifier, Polyspace 製品, Simulink Check, Simulink Coverage, Requirements Toolbox, 組込みシステム, 要求仕様のトレーサビリティ, モデルベースデザイン, コードレビュー, ランタイムエラー, MBD (モデルベース開発)