Simulink Design Verifier を使用した体系的モデル検証について

Simulink^® Design Verifier™ は、隠れた設計エラーの特定、プロパティ証明、および機能テストのテストケース生成を行うための体系的モデル検証に役立ちます。Simulink Design Verifier は形式的手法を使用して、量産コード生成で使用する設計モデルの信頼度を高める、設計の正確性をテストします。

体系的モデル検証は次のようなシナリオで実行できます。

モデルベースデザインを使用して開発されたアプリケーション。この場合は、モデルが機能要件を満たし、かつ、意図しない機能を含んでいないことを証明するために、設計検証を実行します。
制御ソフトウェアを対象とする設計モデルのサブセットの解析。開ループ制御解析の場合、設計モデルの厳格なテストに形式的検証が幅広く使用されます。
要件に対するモデルの反復検証、設計エラーの有無の確認、設計サイクルの初期段階および設計プロセス全体での機能テストの実施。
小さなコンポーネントの単独での体系的検証とユニットレベルのテスト、または、統合された設計モデルのシステムレベルのテスト。

Simulink Design Verifier を使用する状況

制御システムを設計する制御エンジニアについて考えます。設計サイクルにおいて、制御エンジニアはシステム要件に基づき設計モデルを作成します。開発プロセス中に、エンジニアは以下を実行します。

隠れた設計エラーの特定と排除
要件に対するモデルのテスト
モデルおよびコードカバレッジ解析の実行によるテストの完全性の確認
テスト生成とデッドロジック検出を使用した未達カバレッジの解決
ベースラインテストと等価性のテストの実行

Simulink Design Verifier はこれらのモデルおよびコードの検証プロセスをサポートします。また、Requirements Toolbox™、Simulink Coverage™、Simulink Check™、および Simulink Test™ との統合によりモデルとコードの検証を実現します。

モデルベースデザインワークフローでの Simulink Design Verifier の使用

モデル検証では、標準に対するチェック、設計エラーの有無のチェック、プロパティの証明、カバレッジ解析のテストケースの生成を行います。

Simulink Design Verifier では、以下を実行できます。

整数のオーバーフロー、ゼロ除算などの隠れた設計エラーを特定し、意図しない機能をデバッグするための反例を生成する。モデルオブジェクトを正当化したり、解析から除外することもできます。
Requirements Toolbox を使用して、要件に対してモデルを検証する。
モデルカバレッジオブジェクティブを満たすテストケースを生成してモデルカバレッジ (Simulink Coverage)を達成する。
Embedded Coder^® で生成されたコードのテストケースを生成することにより、コードカバレッジ (Embedded Coder)解析を実行する。
既存テストケースを拡張し、未達カバレッジを達成する。
テストケースを Simulink Test と統合してベースラインテストと等価性テストを実行する。
IEC Certification Kit (for IEC 61508 and ISO 26262) と DO Qualification Kit (for DO-178) によって業界標準に対応する。

以下のワークフロー図は、検証と妥当性確認ワークフローのさまざまな段階における Simulink Design Verifier の機能を示しています。

Workflow diagram of SLDV showng various stages of verification and validation.

設計エラー検出およびテスト生成の概要については、コントローラーモデルでの設計エラーの検出および簡略化したクルーズコントロールモデルのテストケースの生成を参照してください。

Simulink Design Verifier の解析の詳細については、バグの検出と対処、テストの生成、モデルのプロパティの証明、および解析結果のレビューを参照してください。

解析結果レポートの作成

レポートを生成し、解析結果をレビューすることもできます。以下の複数の方法で解析結果をレビューできます。

モデルの結果を強調表示して解析結果を一目でレビューする。
テストハーネスモデルを作成して、テストケースのシミュレーションや反例のデバッグを行う。
モデルカバレッジレポートを生成する。
生成されたテストをシミュレーションデータインスペクターに表示する。
解析結果に関する詳細な情報を含む HTML レポートまたは PDF レポートを生成する。