自動スタブによる非互換性処理

自動スタブとは

自動スタブの使用により、Simulink^® Design Verifier™ がサポートしないオブジェクトが含まれるモデルの解析が可能になります。

自動スタブ オプションを有効にすると (既定で有効)、サポートされていないオブジェクトはその実際の動作ではなく、インターフェイスのみが考慮されます。この手法により解析の完了が可能になります。ただし、何らかのサポートされないモデル要素がシミュレーションの結果に影響する場合、一部の解析結果しか得られないことがあります。

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

自動スタブが有効な場合、Simulink Design Verifier 解析でサポートされていないブロックに到達すると、そのブロックは "スタブ" されます。解析はブロックの動作を無視するため、ブロックの出力は任意の値をとることができます。

Trigonometric Function ブロックのスタブ

Simulink Design Verifier は、次の図のように [関数] パラメーターが [acos] に設定されている場合、Trigonometric Function ブロックをサポートしません。

解析時にこのブロックをスタブすると、out_signal は任意の値を受け取ることができ、次の結果になります。

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

関数呼び出しトリガーを含む S-Function ブロックのスタブ

Simulink のモデル例 sfcndemo_sfun_fcncall には、S-Function ブロックがあります。S-Function、sfun_fcncall は、最初の出力端子の 1 番目と 2 番目の要素で Function-Call Subsystem の f1 subsys1 および f2 subsys2 の実行をトリガーします。

Simulink Design Verifier で S-Function のサポートを有効にせず、自動スタブを有効にした場合、解析では S-Function の動作は無視されます。その結果、2 つの Function-Call Subsystem をトリガーするコードは無視され、2 つの達成されないオブジェクティブになります。関数の呼び出しが無視されるため、それらのサブシステムのコンテンツは解析から実質的に削除されます。

Simulink Design Verifier で S-Function のサポートを有効にするには、S-Function および C/C++ コードのサポートの制限事項と考慮事項を参照してください。

自動スタブを使用したモデルの解析

この節では、例として単純な Simulink モデルで自動スタブを使用するワークフローについて説明します。

• モデルの互換性チェック

• 自動スタブの有効化

• 結果の確認

• 完全な結果の達成

以下のモデルには、Simulink Design Verifier と互換性のない Discrete State-Space ブロックが含まれます。

モデルの互換性チェック

Simulink エディターからモデルが Simulink Design Verifier と互換であるかどうかをチェックする方法は 2 つあります。それは Simulink Design Verifier 互換性チェックによるか、Simulink Design Verifier の解析を実行します。

Simulink Design Verifier 互換性チェックを実行するには、次の手順に従います。

• [Design Verifier] タブで、[互換性チェック] をクリックします。

  

• 実行する解析を選択します。

  Simulink Design Verifier の解析を実行するには、[Design Verifier] タブの [モード] セクションで、次のいずれかのオプションを選択します。

  • [設計エラー検出] を選択し、[設計エラー検出] をクリックします。

  • [テスト生成] を選択し、[テスト生成] をクリックします。

  • [プロパティ証明] を選択し、[プロパティ証明] をクリックします。

  最初にモデルの互換性がチェックされます。モデル自体に互換性がない場合 (たとえば、可変ステップ ソルバーが使用される場合)、解析は続行できません。

  互換性のない要素がモデル内に見つかった場合、モデルは解析され、既定ではその互換性のない要素がスタブされます。また、診断ビューアーが開き、互換性のない箇所がリストされます。

  

  メモ

  詳細については、診断の表示を参照してください。

自動スタブの有効化

自動スタブは既定で有効になっています。自動スタブの設定を変更するには、[コンフィギュレーション パラメーター] ダイアログ ボックスのメインの [Design Verifier] ペインのメイン ペインで、[未サポートのブロックおよび関数の自動スタブ化] を選択します。解析を実行すると、スタブが投入され、解析の続行が通知されます。

結果の確認

自動スタブを有効にして解析を実行する場合、必ず結果をレビューしてください。テスト ケース生成の解析後に生成されるこのレポートには、検出されたサポートされないブロックの表があります。

サポートされていないブロック

モデル例について生成された解析レポートでは、スタブが原因でオブジェクティブが未判定であることが示されています。Discrete State-Space ブロックの操作がソフトウェアによって認識されないため、テスト ケースを生成できません。

スタブのため未判定のオブジェクティブ

完全な結果の達成

スタブが原因で解析の結果が完全ではない場合、サポートされないブロックのより正確な定義を指定するためにカスタムのブロック置換を定義できます。詳細については、サポートされていないブロックのブロック置換の手順に従ってください。