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

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

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

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

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

解析	結果に対するスタブの影響
設計エラー検出	スタブ化されたブロックの出力に依存する設計エラーのオブジェクティブが有効と証明された場合、そのオブジェクティブはすべてのシミュレーションで有効になります。この場合、スタブは解析の結果に影響しません。スタブ化されたブロックの出力に依存する設計エラーのオブジェクティブが反証された場合、解析はテストケースを作成できません。解析は、オブジェクティブを反証する出力を生成するスタブ化されたブロックの入力を特定できません。
テストケースの生成	スタブ化されたブロックの出力に依存するテストオブジェクティブが満たされる場合、解析はテストケースを作成できません。解析は、オブジェクティブを達成させる出力を生成するスタブ化されたブロックの入力を特定できません。スタブ化されたブロックの出力に依存するテストオブジェクティブが満たせない場合、そのオブジェクティブを満たすシミュレーションは存在しません。この場合、スタブは解析の結果に影響しません。
プロパティ証明	スタブ化されたブロックの出力に依存する証明オブジェクティブが有効と証明された場合、そのオブジェクティブはすべてのシミュレーションで有効になります。この場合、スタブは解析の結果に影響しません。スタブ化されたブロックの出力に依存する証明オブジェクティブが反証された場合、解析は反例を作成できません。解析は、オブジェクティブを反証する出力を生成するスタブ化されたブロックの入力を特定できません。

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

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

未判定のオブジェクティブがない状態で解析が完了すると、スタブ化されたブロックに関する情報は診断ビューアー、解析レポート、または sldvData に表示されません。例については、未判定のオブジェクティブがない状態での解析の完了を参照してください。
スタブ化が原因で未判定となったオブジェクティブがある状態で解析が完了すると、診断ビューアー、sldvData、および解析レポートにモデル内のスタブ化されたブロックがすべて表示されます。例については、オブジェクティブステータスが [スタブのため未判定] の解析の完了を参照してください。

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

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 つが [スタブのため未判定] ステータスであることが示されます。解析レポートには、解析時に検出されたサポートされないブロックの表があります。

完全な結果の達成

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

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

メモ

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

参考

sldvcompat | sldvrun