Simulink Design Verifier

主な機能

  • Polyspace® および Prover Plug-In® 形式的解析エンジン
  • デッド ロジック、整数および固定小数点のオーバーフロー、ゼロ除算および設計プロパティの違反の検出
  • 機能要求仕様および安全要求仕様をモデル化するブロックおよび関数
  • 機能要求仕様および条件、判定、修正条件判定 (MCDC) を含むモデル カバレッジ オブジェクティブからのテスト ベクトルの生成
  • 解析とデバッグのために違反の例を生成し、プロパティを検証
  • 固定小数点と浮動小数点のモデルをサポート

Simulink Design Verifier を使用すると、Simulink® 環境内でモデル解析を実行することができます。コードを生成することなく、早期に設計の検証と要求仕様の妥当性を確認することができるので、設計プロセス中に検証を実行することが可能になります。Simulink Design Verifier を使用したモデル解析は、シミュレーション結果を形式的手法による解析の入力として使用することによって、シミュレーションを補完します。

Simulink Design Verifier は、組み込み制御設計でよく使用される Simulink および Stateflow® の離散時間のサブセットをサポートします。

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

モデルベース デザインにおける形式的手法

Simulink Design Verifier は、Prover Technology 社の Prover Plug-In 提供の形式的解析技術と、MathWorks の Polyspace 形式的解析エンジンを使用します。これらの技術は数学的に厳密な手順に基づき、テストケースと反例について、考えられるモデルの実行パスを検索します。テスト シナリオと予想結果が具体的なデータ値で表現される従来のテスト手法とは異なり、形式的解析技術では、具体的なデータ値ではなくシステムの振る舞いのモデルを操作できるようになります。システムの振る舞いのモデルには、好ましいシステムの振る舞いと好ましくないシステムの振る舞いが記述されたテスト シナリオと検証オブジェクティブのモデルを含めることができます。このようなモデルを使用して実行された形式的解析はシミュレーションを補完し、設計に対する理解をさらに深める助けとなります。

形式的手法を使用したエラー検出

シミュレーションでのセマンティクスのチェックや解析とは異なり、Simulink Design Verifier で使用される形式的手法では、特定の動的な実行シナリオが発生するかどうか、発生する場合の条件は何かを特定することができます。この情報は、設計や要求仕様の改善に使用したり、デバッグおよび検証のシミュレーションに役立てたりできます。Simulink Design Verifier は、整数オーバーフロー、ゼロ除算、デッド ロジックおよびアサーションの違反などの一般的な設計エラーを検出します。

整数オーバーフローとゼロ除算の検出

Simulink Design Verifier で設計エラー検出モードを使用することで、整数オーバーフローとゼロ除算を検出することが出来ます。解析は自動化されており、ユーザーが何かを追加入力する必要はまったくありません。すべてのブロック上の全信号に対する許容範囲が提供され、問題の根本原因を見つけ出すよう導いてくれます。解析終了後、モデルで直接または HTML 形式のレポートで結果を確認することができます。

モデルでは、ブロックは緑色、黄色、赤色でマークされています。緑色のブロックは、整数オーバーフローまたはゼロ除算を引き起こさないことが証明されています。黄色のブロックは、解析で最終的な結果が得られない、または解析時間の限度を超えたことを示します。モデルの実行パスでエラーが検出された場合、整数オーバーフローとゼロ除算を発生させる可能性がある、そのパス上のそれ以降のすべてのブロックは黄色でマークされます。

赤色のブロックには、設計エラーがあります。赤色のブロックに対しては、Simulink Design Verifier はシミュレーションまたはテスト中に問題を再現できるテスト ケースを生成します。 テスト ケースを呼び出して、Simulink 内から直接シミュレーションを実行することができます。

デッド ロジックの検出

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

テスト生成解析終了後、モデルはテスト生成の基準に従って色分けされます。シミュレーションでアクティブにできないロジックが含まれているモデル オブジェクトは赤色、シミュレーションで完全にアクティブになるロジックを含んだモデル オブジェクトは緑色でマークされます。Simulink Design Verifier は、シミュレーション中にデッド ロジックを再現できるテスト ケースを生成します。

Dead logic in a Stateflow chart detected by Simulink Design Verifier.
Simulink Design VerifierはStateflow チャートの遷移を赤色に強調表示しています。条件 “press < zero_thresh” が false になることは決してないため、この遷移でデッド ロジックが発生します。

アサーション違反の検出

Simulink Design Verifier でプロパティ証明モードの違反検出設定を使用して、アサーション違反を検出します。Simulink Design Verifier は、シミュレーション時に解析設定で指定されているタイム ステップ数以内で有効なシナリオがアサーションをトリガーできるかどうかを検証します。たとえば、逆推力アクチュエータが有効で、飛行ステータス インジケーターの値が “true” の場合にトリガーするアサーションを構築することができます。有効なシナリオで違反する可能性のあるアサーションは赤色で強調表示され、アサーションをトリガーするテスト ベクトルが生成されます。Simulink で利用できるアサーションに加え、Simulink Design Verifier では解析の制約を定義するための追加ブロックが提供されるため、設計動作を漏れなく解析してシミュレーションを実行する前に設計の不具合を検出することができます。

要求仕様に対する設計の検証

離散システムの機能要求仕様は、システムに予期される動作と発生してはならない動作についての明示的なステートメントとなっています。発生してはならない動作は、安全要求仕様と呼ばれています。

Simulink での機能要求仕様の表現

設計がこれらの要求仕様に従って動作することを形式的に検証するには、まず要求仕様のステートメントを人間の言語から形式解析エンジンが理解できる言語に翻訳する必要があります。Simulink Design Verifier を使用すると、SimulinkMATLAB® 関数および Stateflow を使用して形式的な要求仕様を表現することができます。Simulink での各要求仕様には、1 つまたは複数の検証オブジェクティブが関連付けられています。これらの検証オブジェクティブは、設計が機能要求仕様と安全要求仕様を満たすかどうかのレポートに使用されます。

Simulink Design Verifier には、検証オブジェクティブの定義と整理に使用できる一連の基本ブロックと関数が用意されています。ブロック ライブラリには、テスト オブジェクティブ、証明オブジェクティブ、アサーション、制約用のブロックと関数、および時相で検証オブジェクティブをモデル化するための専用の時相演算子が含まれています。

個々の要求仕様とそれぞれに関連する検証オブジェクティブをライブラリにまとめて、設計とは個別に管理、確認することができます。

Simulink Design Verifier library of property examples.
Simulink Design Verifier のプロパティ ライブラリの例。

Simulink Verification and Validation™ で Simulink Design Verifier を Requirements Management Interface と併用すると、要求仕様と検証オブジェクティブを取得するために使用するブロックと関数を、Simulink 外にあるさらにレベルの高い要求仕様記述とリンクすることができます。

要求仕様に対する設計の実証

要求仕様と検証オブジェクティブが検証モデルに取り込まれたら、形式的手法を使用して設計の妥当性を証明することができます。

機能要求仕様を検証してシステムを望ましい状態へ導くため、Test Objective ブロックと MATLAB 関数を使用してテスト オブジェクティブを定義することができます。テストの生成中、Simulink Design Verifier は指定されたオブジェクティブを満たす有効なテスト ケースを見つけ出そうとします。オブジェクティブを満足させることができない場合、設計は特定の解析制約に対して要求される機能を実行することができません。

設計が安全要求仕様に対して妥当であることを検証するには、Proof Objective ブロックと MATLAB 関数を使用して証明オブジェクティブを定義します。解析中、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、MATLAB 関数および Stateflow で表現されている要求仕様は、設計と並行してシミュレーションすることができます。それらを使用して SIL モードまたは PIL モードで同時にシミュレートしながら生成されたコードを検証することもできます。モデル カバレッジ ツールはシミュレーション中に検証オブジェクティブのアクティベーションに関する情報を蓄積し、Simulink Design Verifier カバレッジ メトリックによってカバレッジ結果を提供します。違反時にシミュレーションを停止する安全要求仕様を表す証明オブジェクティブを使用して、根本的な原因の解析とデバッグを高速化できます。

モデル カバレッジの解析

Simulink Design Verifier は、Simulink および Stateflow モデルでアルゴリズムとロジックを解析し、業界標準で信頼性の高いシステムを開発するために必要なテスト ケースとパラメーターを生成します。構造カバレッジ基準のテストの生成には、条件、判定、修正条件判定カバレッジ (MC/DC) が含まれています。

テストの生成

モデル カバレッジのテストの生成は、手動作成またはシステム全体のシミュレーション中に収集された要求仕様に基づくテストを補強します。この手法により、Simulink Design Verifier は既存のモデル カバレッジ情報を使用して、要求仕様に基づくテストで満足させられなかったすべてのカバレッジ オブジェクトを満たす追加のテスト ベクトルを生成します。

Visual display of a generated test vector that activates previously untested functionality.

まだテストされていない機能をアクティブにする、生成されたテスト ベクトルの表示。

これらのテスト ベクトルを使用して、満たされていない要求仕様への理解を深め、さらに完全なテスト ハーネスを作成することができます。多数の Inport と Outport のあるモデルのテストを簡略化するため、Simulink Design Verifier は未使用の信号を特定し、それらをテスト ハーネスから自動的に削除します。

生成されたすべてのテスト ベクトルは、シミュレーション、SIL または PIL でのテスト実行時に入力として直接使用できる MATLAB 構造体としてキャプチャされます。収集されたテスト データを使用して、テスト ハーネス モデルを生成することもできます。

生成されたテスト ベクトルの検証

構造カバレッジ基準を満たす生成されたテスト ベクトルを検証するには、Simulink Verification and Validation で提供されるモデル カバレッジ ツールを使用できます。このツールはシミュレーションを監視し、形式的解析中に報告されるオブジェクティブが達成されたかどうかを測定します。モデル カバレッジ ツールは、条件、判定および MC/DC カバレッジのカバレッジ オブジェクティブに加え、シミュレーション中に記録されたテスト オブジェクティブ、証明オブジェクティブ、仮定、制約、ルックアップ テーブルおよび信号範囲もレポートします。

Simulink Design Verifier はTÜV SÜDによって、ISO 26262IEC 61508、または EN 50128 標準に準拠した開発プロセスとして認証されています。

生成されたコードでのテスト カバレッジの解析

Simulink Design Verifier には、SIL および PIL のコードに対して生成されたテスト ケースの実行を自動化するテスト オートメーション関数が用意されています。Simulink Design Verifier のコード検証関数には、Embedded Coder™ が必要となります。テストの実行中に、Embedded Coder で利用できるコード カバレッジ ツールを統合してコード カバレッジを収集できます。

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

Simulink R2014b 新機能紹介 ~Simulinkプロダクトファミリ~

Web セミナーを表示する