このページの内容は最新ではありません。最新版の英語を参照するには、ここをクリックします。

Simulink Design Verifier 入門

設計エラーの特定、要件への準拠性の証明、およびテスト生成

Simulink® Design Verifier™ は形式的手法を使用することで、モデル内の隠れた設計エラーを特定します。整数のオーバーフロー、デッド ロジック、配列アクセスにおける違反、およびゼロ除算を引き起こすブロックをモデル内で検出します。設計が機能要件を満たしていることを形式的に検証できます。各設計エラーまたは各要件違反について、デバッグ用のシミュレーション テスト ケースを生成します。

Simulink Design Verifier は、モデル カバレッジおよびカスタム オブジェクティブ用のテスト ケースを生成することで、要件に基づく既存のテスト ケースを拡張します。これらのテスト ケースによりモデルは条件、判定、改良条件判定 (MCDC) およびカスタムのカバレッジ オブジェクティブを達成できます。カバレッジ オブジェクティブのほかに、カスタム テスト オブジェクティブを指定して、要件に基づくテスト ケースを自動生成できます。

業界標準には、IEC Certification Kit (for IEC 61508 and ISO 26262) と DO Qualification Kit (for DO-178) によって対応しています。

チュートリアル

注目の例

デッド ロジック解析に対する結果の解析

デッド ロジック解析に対する結果の解析

この例は、sldvexCommonCausesOfDeadLogic モデルを使用して、デッド ロジックの原因となっている可能性のある個所を分離する方法を示します。デッド ロジックの検出では、モデル要素が非アクティブで残される原因となる、モデル内の到達不可能なオブジェクティブを見つけます。

クルーズ コントロール のプロパティ証明ワークフロー

クルーズ コントロール のプロパティ証明ワークフロー

この例では、Simulink® Design Verifier™ のプロパティ証明解析を使用した、プロパティ違反の検出方法を示します。安全要件をプロパティとしてモデル化してから、要件に対して設計モデルを検証します。

要件に基づくテストに対する仕様モデルの使用

要件に基づくテストに対する仕様モデルの使用

要件に対して設計モデルを検証する体系的なアプローチに従います。

ビデオ

Simulink Design Verifier とは
Simulink Design Verifier の紹介

How to Use Simulink Design Verifier to Automatically Detect Design Errors in Your Simulink Models
Simulink Design Verifier を使用して設計のエラーを検出し、エラーが検出された場合は、Simulink Design Verifier の可視化機能を使用してそのエラーをデバッグする方法を調べる。

DO-178C Workflow for Automatic Test Vector Generation
DO-178C とその補完内容に準拠するために、Simulink Design Verifier を使用してテスト ベクトルを自動生成し、Simulink Coverage によって収集された未達モデル カバレッジを解析する。

How to Debug a Property Proving Counterexample
Simulink Design Verifier™ でのプロパティ証明は、形式的手法を使用して特定のプロパティが常に有効かどうかを証明する静的な解析手法です。この手法は、設計で実装されている特定の要件が常に満たされることを形式的に検証するのに役立ちます。

要件に基づくテスト ワークフロー
テスト シーケンスを使用してテストを作成する方法、形式的評価を定義する方法、テスト ケースを要件にリンクする方法、テスト スイートを実行する方法、および未達モデル テスト カバレッジを解析する方法を説明する。