Main Content

このページの翻訳は最新ではありません。ここをクリックして、英語の最新版を参照してください。

Simulink Design Verifier 入門

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

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

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

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

チュートリアル

注目の例

整数オーバーフロー エラーの検出

整数オーバーフロー エラーの検出

この例では、設計エラー検出解析を使用して、モデル内の整数オーバーフロー エラーを検出する方法を示します。Simulink® Design Verifier™ は、結果として整数オーバーフローに至る可能性のあるモデル構造を特定し、シミュレーション中に整数オーバーフローが発生することがないと証明するか、または、整数オーバーフロー エラーを示すテスト ケースを生成するかのいずれかを行います。

スクリプトを開く
クルーズ コントロール のプロパティ証明ワークフロー

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

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

例を開く
クルーズ コントロール テストの生成

クルーズ コントロール テストの生成

この例では、すべてのモデル カバレッジを達成するテスト ケースの生成方法を示します。既定で、Simulink® Design Verifier™ は最小ステップでオブジェクティブを達成するテスト ケースを生成します。いずれか 1 つのテスト オブジェクティブにより、PI コントローラーの離散積分器がその上限を超過するように強制されます。制約なしで Simulink Design Verifier を実行する場合、速度を 500 に強制することにより、この制限は単一のステップで超過します。速度の制約により、テスト ケースの値は 0 ～ 100 の間で制限されます。これにより、テスト ケースはいくつかのサンプルをとり、積分器の制限を超えるように強制されます。

スクリプトを開く

ビデオ

Simulink Design Verifier とは
Simulink Design Verifier の紹介

要件と高度なモデル チェックのワークフロー
Simulink で要件を管理し、高度なモデル チェックを実行して、モデルにランタイム エラーがないかチェックする。

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