Simulink Design Verifier

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

シミュレーションでのセマンティクスのチェックや解析とは異なり、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 Design Verifier

評価版ソフトウェアを入手する

モデルベースデザインの基本環境クイック・デモ

Web セミナーを表示する