Accelerating the pace of engineering and science

Simulink Design Verifier

主な機能

  • 機能的な要求仕様と条件、判定および MCDC などのモデル カバレッジ オブジェクティブからテスト ケースの入力を生成
  • デッド ロジック、整数や固定小数点のオーバーフロー、配列アクセス違反、ゼロ除算、設計要件違反などを検出
  • 機能的な要求仕様やセキュリティに関する要求仕様をモデリングするための検証ブロック
  • 解析とデバッグのために違反の例を生成し、プロパティ検証を実施
  • 大規模モデルの機能的な依存関係と問題のある動作を解析するためのモデル スライサー
  • 固定小数点および浮動小数点モデル用の Polyspace® および Prover® 形式検証エンジン

Simulink Design Verifier 概要
Identify design errors, generate test cases, and verify designs against requirements using Simulink Design Verifier™.

Simulink Design Verifier™ を使用すると、コードを生成する必要なしに、設計の初期段階で設計と要求仕様を検証することができます。また、Simulink® 環境内で設計のロバスト性を向上させることを支援します。数学的に厳密な形式的手法を使用して、制御ロジック、S-Function および MATLAB® コードを解析できます。テスト シナリオと予想される結果が具体的なデータの値で示される従来のテスト手法とは異なり、形式的検証手法では、システムの挙動モデルを使用することができます。形式的検証では、ソフトウェアに実行時エラーが含まれるかどうかなど、ソフトウェアの特定の属性を証明できるため、システムの要求仕様に対する理解が深まります。

設計エラー検出

Simulink Design Verifier を使用すると、特定の動的実行シナリオが発生するかどうか、およびそのシナリオが発生する条件を見つけることができます。整数オーバーフロー、ゼロ除算、デッド ロジック、範囲外の配列などの設計エラーを検出できます。シミュレーションに基づいたテストの前に、設計早期の段階にこれらのエラーを検出することにより、その後のコストのかかる修正を回避できます。

Design error detection in a model using Simulink Design Verifier.
設計エラー検出。赤色で強調表示されているブロックには設計エラーがあり、緑色で強調表示されているサブシステムには設計エラーがないことが証明されています。

設計エラー検出は完全に自動的に行われ、モデル上で結果を直接確認するか、HTML レポートで結果を確認できます。すべてのブロックの全信号の許容範囲が提供されるため、問題の根本的原因が見つけやすくなります。モデルでは、ブロックが緑色、オレンジ色または赤色でマークされます。緑色はエラーが検出されなかったことを示し、オレンジ色は解析が時間内に終了しなかったことを示し、赤色は設計エラーのあるブロックを示しています。Simulink Design Verifier は、テスト ケースの入力を自動的に生成し、赤色の各ブロックのエラー シナリオを再現します。Simulink でこれらのテスト入力を使用して、エラーが発生した条件を把握してデバッグすることができます。

デッド ロジックの検出

Dead logic in a Stateflow chart detected by Simulink Design Verifier.
Simulink Design Verifier により Stateflow チャートの遷移におけるデットロジックの部分は赤色で強調表示されます。条件 "press < zero_thresh" が偽になることはないため、この遷移でデッド ロジックが発生します。

デッド ロジック検出モードを使用すると、モデル内に使用廃止されたオブジェクト、または、実行中にアクティブにならないと証明されたオブジェクトを検出することができます。多くの場合、デッド ロジックは、設計のエラーまたは要求仕様のエラーによって発生します。コードの生成中、デッド ロジックはデッド コードの生成につながります。シミュレーションでアクティブにならないロジックが含まれているモデル オブジェクトは赤色、シミュレーションで完全にアクティブになるロジックを含んだモデル オブジェクトは緑色でマークされます。多数のシミュレーションを実行したとしても、特定の動作がアクティブにならないと証明することは難しいため、シミュレーションのみのテストでデッド ロジックを検出することは困難です。

テスト ケースの入力の生成

実装モデルのみで入出力挙動を検証したとしても、設計の正確さは保証されません。機能テストはモデルを検証する上で有効な初期ステップですが、これらのテストは基本的に要求仕様より生成されたものであり、不完全な場合があります。設計のロバスト性を向上させるために、モデル カバレッジなどの構造検証手法を使用して、モデルの使用されていないシミュレーション経路を特定することができます。本質的に、モデル カバレッジでは、テスト ケースでモデルがどの程度実行されるかを測定し、テスト ケースで実行された経路の割合を示します。テストされていない経路を調査することにより、潜在的な設計エラーを検出することができます。

既存のテスト ケースを拡張し、フルモデル カバレッジを達成
Simulink Design Verifier™ でテスト生成するための形式的手法を使用して、既存のテスト ケースを活用し、フル カバレッジを達成します。

Simulink Design Verifier は、形式的手法とヒューリスティックな手法を組み合わせて、モデル カバレッジとカスタム ユーザー基準のためのテスト ケースを生成します。モデル カバレッジのテスト ケース生成により、手動で作成された、またはシステム全体のシミュレーション中に収集された要求仕様ベースのテストの入力が強化および拡張されます。条件、判定および MCDC カバレッジに対するカバレッジ オブジェクティブに加えて、カスタム テスト オブジェクティブを指定して、要求仕様ベースのテスト ケースを生成することもできます。

要求仕様ベースのテスト
Simulink Design Verifier™ を使用して、システム要件のモデルからテスト ケースを生成します。

テスト生成アドバイザーを使用して、テスト生成のためのモデル コンポーネント (アトミック サブシステムとモデル ブロック) を選択できます。テスト生成アドバイザーは高度な解析を実行することにより、特に、大規模なモデル、複雑なモデルまたはテスト生成の互換性が不確実なモデルについて、テスト生成の前にモデルの理解を深めることを支援します。生成されたすべてのテスト ケースの入力は、シミュレーション、SIL または PIL のテスト実行用の入力として直接使用できる MATLAB 構造体としてキャプチャされます。また、収集されたテスト データを、Simulink Test™ および関連するテスト ハーネスで使用することができます。テストの実行中に、コード カバレッジを収集するために、Embedded Coder® で使用できるサードパーティのコード カバレッジ ツールと統合することができます。

Simulink Design Verifier は ISO 26262IEC 61508 または EN 50128 規格に準拠する必要がある開発プロセスで使用することがTÜV SÜD によって認定されています。

Visual display of a generated test vector that activates previously untested functionality.
テスト生成アドバイザー:階層ビューで表示されたモデルまたはモデル コンポーネントのテスト生成の互換性、カバレッジ オブジェクティブ、デッド ロジックの概要

モデル スライサーによる問題のある動作の分離

Simulink Design Verifier は、動的解析と静的解析の組み合わせ使用して依存関係をトレースすることにより、モデルの対象動作を分離します。依存関係の解析には、ブロック、信号およびモデル コンポーネントの依存関係を判定することが含まれます。階層のレベルと設計の複雑さを考えると、大規模なモデルでは、この解析は時間のかかる作業となります。モデル スライサーを使用すると、特定の動作に影響を及ぼしているモデルの部分を把握しやすくなります。静的解析を使用して、実行される可能性のあるすべてのシミュレーション経路のモデル依存関係を特定することができます。一方で、シミュレーションに基づいた解析を使用すると、シミュレーション中にアクティブになる経路のみが強調表示されます。

依存関係の解析は、開始点から上流方向、下流方向または双方向に伝播します。端子、信号およびブロックの機能的な依存関係を強調表示およびトレースし、解析のために大規模なモデルをより小さなスタンドアロン モデルにスライスすることができます。また、サブシステムの出力に影響を及ぼしているブロックを表示し、複数のスイッチと論理ブロックを経由する信号の経路をトレースすることができます。

Testing and debugging complex models
複雑なモデルのテストとデバッグ。モデルの対象領域を特定し、詳細な解析とデバッグのためにスライス モデルを生成します。

要求仕様ベースの検証

設計が特定の機能要件または安全要件に従って動作することを形式的に検証するには、最初に、要求仕様のステートメントを人間の言語から形式的解析エンジンが理解できる言語に変換する必要があります。Simulink Design Verifier では、MATLAB 関数、Simulink および Stateflow® を使用して形式的要求仕様を表現することができます。Simulink の各要求仕様には、関連付けられた 1 つ以上の検証オブジェクティブがあります。要求仕様と検証オブジェクティブがキャプチャされると、形式的手法によって、要求仕様と検証オブジェクティブを使用して設計の正確さを証明することができます。

たとえば、フライト追跡システムでは、逆噴射装置のアクチュエータが作動し、フライトステータス インジケーターの値が "true" になると常にトリガーされるアサーションまたは証明オブジェクティブを作成する場合があります。Simulink Design Verifier は、不適切な動作を引き起こす可能性のあるすべての入力条件を検証し、検証結果をレポートします。任意の証明オブジェクティブのために、設計の有効性を証明するか、設計が安全要件に違反していることを証明できます。違反が検出されると、Simulink Design Verifier は、違反を再現できるテスト ケースを生成します。

Simulink Design Verifier report for verifying a design against safety requirements represented with proof objectives.
証明オブジェクティブで表されている安全要件に照らし合わせて設計を検証する Simulink Design Verifier のレポート。このレポートには、設計の有効性が証明されたオブジェクティブのリストと、解析で反例として検出されたオブジェクティブのリストが示されています。

Simulink Design Verifier と Simulink Verification and Validation™ の Requirements Management Interface を併用すると、要求仕様と検証オブジェクティブをキャプチャするために使用されるブロックと関数を、Simulink 外部の高度な文書化された要求仕様にリンクすることができます。

製品評価版の入手
または製品の購入

医療機器開発におけるモデルベースデザイン

Web セミナーを表示する