Simulink Design Verifier 入門

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

Simulink® Design Verifier™ は形式的手法を使用することで、モデル内の隠れた設計エラーを特定します。整数のオーバーフロー、デッド ロジック、配列アクセスにおける違反、ゼロ除算など、実行時エラーや望ましくない動作の原因となるモデル内の演算を検出します。複雑なモデルの結果を迅速に得るために、解析は複数の CPU コアに分散されます。

Simulink Design Verifier は形式的検証を実行し、設計が機能要件を満たし、安全性要件に違反していないことを証明します。形式的解析は、要件の整合性と完全性についても検証します。各設計エラーまたは各要件違反について、デバッグ用のシミュレーション テスト ケースが生成されます。

Simulink Design Verifier を使用することで、テスト ベクトルを自動生成してモデル カバレッジおよびコード カバレッジを達成できます。これらのテスト ベクトルはモデルを駆動し、判定、条件、および改良条件判定 (MC/DC) のカバレッジ メトリクスを達成します。

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

チュートリアル

注目の例

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

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

解析時にデッド ロジックになる可能性のある原因を特定する。

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

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

この例では、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™ でのプロパティ証明は、形式的手法を使用して特定のプロパティが常に有効かどうかを証明する静的な解析手法です。この手法は、設計で実装されている特定の要件が常に満たされることを形式的に検証するのに役立ちます。

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