体系的モデル検証における Simulink Design Verifier の使用
自動車分野や航空宇宙分野の制御エンジニアは、基礎となる制御アルゴリズムがオペレーション ライフサイクル全体を通して目的の動作をしていることを確認する必要があります。
Simulink® Design Verifier™ は、隠れた設計エラーの特定、プロパティ証明、および機能テストのテスト ケース生成を行うための体系的モデル検証に役立ちます。Simulink Design Verifier は形式的検証手法を使用して、設計の正確性をテストし、量産コード生成で使用する設計モデルの信頼度を高めます。たとえば、エンジニアは開発ライフサイクルで検証と妥当性確認を実行して、次のことを確認できます。
エンジン マネジメント システムが、動作中に意図しない加速やエンストなどの望ましくない動作を引き起こさない。
ブレーキとステアリングを制御する先進運転支援システム (ADAS) アプリケーションが、どのような条件下でも適切に動作する。
自動操縦システムが、考えられるすべての飛行条件と入力に正しく対応する。
飛行制御システムが安定しており、飛行中に致命的な障害を防ぐように対応する。
モデル設計者とテスト エンジニアは、モデルの開発フェーズの進展において Simulink Design Verifier を使用して、検証と妥当性確認を実現します。

Simulink Design Verifier の機能
Simulink Design Verifier には、次のような機能が用意されています。
| 機能 | 説明 |
|---|---|
| 機能要件の解析 |
詳細については、要件に基づくテストに対する仕様モデルの使用を参照してください。 |
| テスト生成 |
詳細については、を参照してください。 |
| 設計エラー検出 |
詳細については、設計エラー検出とはを参照してください。 |
| プロパティの証明 |
詳細については、Simulink Design Verifier を使用したモデル プロパティの証明を参照してください。 |
| インクリメンタルな分析、フィルター適用、および正当化 |
|
生成されたコードの解析 |
|
認定または準拠 | 生成されたアーティファクトを使用して、自動車向けの ISO 26262 や航空宇宙向けの DO-178C などの業界標準に準拠します。 |
Simulink Design Verifier の使用方法
Simulink Design Verifier を使用するための主要な手順は次のとおりです。

モデルの準備: 解析用にモデルを準備します。
テスト ケースの生成、設計エラー検出、プロパティ証明解析などの解析モードを選択します。
解析パラメーターを構成し、解析とモデルの互換性をチェックします。詳細については、Simulink Design Verifier の解析の基礎を参照してください。
モデル設定の構成と解析の実行: モデル設定を指定し、解析のニーズに関連する解析を実行します。
最大解析時間、カバレッジ モード、ランタイム エラー モード、手法、その他の解析のコンフィギュレーション パラメーターを選択します。
解析を実行します。
結果の確認: 生成された結果を表示します。
解析の完了後に Simulink Design Verifier によって強調表示されたモデルの結果を検証します。
オブジェクティブのステータスを確認し、フォローアップ アクションを定義します。
解析レポートを生成します。
結果のエクスポート: 結果から得られた洞察を使用してモデルまたは解析設定を調整します。
シミュレーション用のハーネスを作成します。
テスト ケースを Simulink Test™ にエクスポートします。
詳細については、Simulink Design Verifier の解析の基礎を参照してください。
モデルベース デザインにおける Simulink Design Verifier
以下の図は、検証と妥当性確認ワークフローのさまざまな段階における 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 は、IEC Certification Kit (for IEC 61508 and ISO 26262) と DO Qualification Kit (for DO-178) によって業界標準への準拠もサポートしています。