自動スタブによるモデルの複雑度の処理

R2026b

Simulink® Design Verifier™ におけるスタブとは、解析を可能にするためにモデルの特定の部分をより単純な表現である "スタブ" に置き換える処理のことです。自動スタブにより、複雑な要素が含まれるモデルの解析が可能になります。Simulink Design Verifier は、解析期間にわたって、または解析の特定の段階でのみ要素をスタブ化します。たとえば、Float Extract Bits ブロックを解析全体にわたってスタブ化する一方で、Trigonometric Function ブロックを特定の段階 (Simulink Design Verifier がデッド ロジックを特定するためにモデルを解析する場合など) でのみスタブ化できます。Simulink Design Verifier の解析では、スタブ化されたブロックの出力は下流ブロックの評価時に可能な全範囲内の任意の値を取ることができると仮定されます。

自動スタブを使用して得られた解析結果は、スタブの使用の影響を受ける可能性があります。スタブ化により、解析がブロックの動作を完全に探索することが妨げられ、その結果、一部のオブジェクティブが未判定または未カバーになる可能性があります。スタブによる影響を受けるオブジェクティブは、[スタブのため未判定] ステータスで示されます。

自動スタブの機能について

自動スタブにより、モデルの特定の部分の解析が制限される可能性があり、Simulink Design Verifier は残りのコンポーネントを引き続き解析します。次の表は、解析結果に対するスタブの影響をまとめたものです。

解析結果に対するスタブの影響

設計エラー検出

  • 設計エラーのオブジェクティブがスタブ化されたブロックの出力に依存しており、解析によってそのオブジェクティブが有効であると証明された場合、そのオブジェクティブはすべてのシミュレーションにおいて有効なままになります。この場合、スタブは解析結果に影響しません。

  • 反証された設計エラーのオブジェクティブがスタブ化されたブロックの出力に依存している場合、解析では、反証された出力を生成した入力を解釈できないため、反例は生成されません。

テスト ケースの生成

  • 達成可能なテスト オブジェクティブがスタブ化されたブロックの出力に依存している場合、解析では、そのテスト オブジェクティブを達成する出力を生成した入力を解釈できないため、テスト ケースは生成されません。

  • スタブ化されたブロックの出力に依存するテスト オブジェクティブが満たせない場合、そのオブジェクティブを満たすシミュレーションは存在しません。この場合、スタブは解析の結果に影響しません。

プロパティ証明

  • 証明オブジェクティブがスタブ化されたブロックの出力に依存しており、解析によってそのオブジェクティブが有効であると証明された場合、そのオブジェクティブはすべてのシミュレーションにおいて有効なままになります。この場合、スタブは解析結果に影響しません。

  • 反証された証明オブジェクティブがスタブ化されたブロックの出力に依存している場合、解析では、反証可能な出力を生成した入力を解釈できないため、反例は生成されません。

自動スタブの解析結果のレビュー

Simulink Design Verifier はブロックをスタブ化し、これらのブロックの抽象化された動作に基づいて解析結果を提供します。

未判定のオブジェクティブがない状態での解析の完了

Simulink Design Verifier の解析では、スタブが適用されている場合でも、すべてのオブジェクティブのステータスが判定されます。この場合、結果は通常どおりに表示でき、スタブが発生したことを示す通知は表示されません。

出力が Sqrt ブロックに依存する Switch ブロックをもつ次のモデルについて考えます。それぞれのスイッチ位置の出力は、1-D Lookup Table ブロックによって決定されます。テスト生成解析を実行すると、Simulink Design Verifier は Sqrt ブロックをスタブします。スタブ動作は他のブロックに影響を与えず、解析によって完全な結果が生成され、6 つすべてのオブジェクティブが達成されます。結果は完全で、解析レポートにはスタブ化された Sqrt ブロックに関する詳細は表示されません。

Simulink model named sldvdemo_sqrt_block showing a 1-D Lookup Table block,a Sqrt block, a Switch block, a min max block, and a Relational Operator block. Results window highlights that all the objectives are satisfied, indicating complete results. Below, a snippet from Simulink Design Verifier report listing the objectives for the analysis.

オブジェクティブ ステータスが [スタブのため未判定] の解析の完了

オブジェクティブ ステータスがスタブ化の影響を受ける場合、Simulink Design Verifier の解析レポートには、ブロックがサポートされていないか、オブジェクティブ ステータスが [スタブのため未判定] であることが示されます。診断ビューアーには、Simulink Design Verifier でスタブ化されたブロックの動作を抽象化できるかどうかに関係なく、スタブ化されたすべてのブロックに関する警告が表示されます。

解析時にスタブされる Math Function ブロックを含むモデルについて考えます。設計エラー検出解析を実行すると、診断ビューアーに、解析が Math Function ブロックの影響を受けているという警告が表示されます。これは、ブロック内の一部の条件がブロックへの入力に基づいてトリガーされるためです。ブロックが解析時にスタブ化された場合、Simulink Design Verifier は使用可能な入力によって特定の条件に到達できることがありますが、他の条件には到達できない可能性があります。

[結果] ダイアログ ボックスには、2 つのオブジェクティブのうち 1 つが [スタブのため未判定] ステータスであることが示されます。解析レポートには、解析時に検出されたサポートされないブロックの表があります。

Simulink model named mStubbed_block showing a Math Function block. Results window highlights that one out of two objectives is undecided due to stubbing, indicating incomplete results. Below the Diagnostic Viewer displays a warning that the Math Function block is configured to operate as a function exp, which may impact analysis. On the right, a snippet from Simulink Design Verifier report listing the Math Function as an unsupported block of type Math explaining that unsupported blocks can cause partial analysis.

完全な結果の達成

サポートされないブロックのより正確な定義を指定するためにカスタムのブロック置換を定義できます。詳細については、ブロック置換ルールのテンプレートの手順に従ってください。

追加のガイダンスについては、Resolve Undecided Objective Statuses Resulting from Model Complexityのスタブに関する回避方法を参照してください。

メモ

自動スタブは、コード生成プロセスやその結果生成されるコードには影響しません。生成されたコードにはモデルの解釈が反映されます。

参考

|

トピック