メインコンテンツ

ブロック置換を使用した解析の実行

ブロック置換を使用すると、代替ブロックの独自のライブラリとカスタムのブロック置換ルールを定義できます。ブロック置換を使用すると、次のことができます。

  • モデル内のサポートされないブロックの存在など、非互換性の回避。

  • 次のような、ブロックの解析向けカスタマイズ:

    • 入力信号への制約の追加

    • 出力信号へのオブジェクティブの追加

    • サブシステムまたは Model ブロックのコンテンツ消去による解析の単純化

ブロック置換を実行すると、モデルのコピーが作成され、元のモデルを変更することなくそのコピー内でブロックが置換されます。このように、容易にモデルを解析用にカスタマイズできます。

Simulink® Design Verifier™ ソフトウェアは、以下を使用してモデル内のブロックを自動的に置き換えます。

  • 代替ブロックのライブラリ

  • 置換するブロックおよび置換条件の定義ルール

任意のブロックが任意の組み込みブロック、ライブラリ ブロックまたはサブシステムに置き換えられます。

組み込みブロック置換

Simulink Design Verifier ソフトウェアでは、一連のブロック置換ルールと、対応する代替ブロックのライブラリを提供します。モデルの解析時にこれらの組み込みブロック置換が使用されます。これらは独自のブロック置換の作成方法を学ぶために検討できる例として役立ちます。

出荷時の既定のルールに対応する代替ブロックのライブラリは次です。

matlabroot/toolbox/sldv/sldv/sldvblockreplacementlib

以下の表は出荷時の既定のブロック置換ルールの一覧です。これらは matlabroot\toolbox\sldv\sldv\private フォルダーで見ることができます。それぞれの出荷時の既定のブロック置換ルールには 2 つの実装があります。_normal.m で終わるファイル名のルールは、ブロックを Subsystem ブロックに置き換えます。詳細については、Design Verifier ペイン: ブロック置換を参照してください。

ファイル名

説明

blkrep_rule_lookup_normal.m

1-D Lookup Table ブロックを、[ブレークポイント] パラメーターで指定された各ブレークポイントおよび区間に対するテスト オブジェクティブを含んだ実装に置換するルール。

blkrep_rule_lookup2D_normal.m

Test Condition ブロックまたは Proof Assumption ブロックを 2-D Lookup Table ブロックの入力端子に追加するルール。それぞれの Test Condition または Proof Assumption ブロックは信号値を、対応するブレークポイント ベクトルで指定された間隔に制約します。

blkrep_rule_mpswitch2_normal.m

Test Condition ブロックまたは Proof Assumption ブロックを、[データ端子数] パラメーターが 2Multiport Switch ブロックの制御入力端子に追加するルール。Test Condition ブロックまたは Proof Assumption ブロックは信号値を [1, 2] の区間 (ブロックが 0 ベースのインデックスを使用している場合は [0, 1]) に制約します。

blkrep_rule_mpswitch3_normal.m

Test Condition ブロックまたは Proof Assumption ブロックを、[データ端子数] パラメーターが 3Multiport Switch ブロックの制御入力端子に追加するルール。Test Condition ブロックまたは Proof Assumption ブロックは信号値を [1, 3] の区間 (ブロックが 0 ベースのインデックスを使用している場合は [0, 2]) に制約します。

blkrep_rule_mpswitch4_normal.m

Test Condition ブロックまたは Proof Assumption ブロックを、[データ端子数] パラメーターが 4Multiport Switch ブロックの制御入力端子に追加するルール。Test Condition ブロックまたは Proof Assumption ブロックは信号値を [1, 4] の区間 (ブロックが 0 ベースのインデックスを使用している場合は [0, 3]) に制約します。

blkrep_rule_mpswitch5_normal.m

Test Condition ブロックまたは Proof Assumption ブロックを、[データ端子数] パラメーターが 5Multiport Switch ブロックの制御入力端子に追加するルール。Test Condition ブロックまたは Proof Assumption ブロックは信号値を [1, 5] の区間 (ブロックが 0 ベースのインデックスを使用している場合は [0, 4]) に制約します。

blkrep_rule_switch_normal.m

Switch ブロックを、テスト オブジェクティブを含む実装で置換するルール。最初と 3 番目の入力端子の値が異なる場合、それぞれのスイッチ位置を確認する必要があります。

blkrep_rule_switch_nonvir_normal.m

非バーチャル バス入力をもつ Switch ブロックを、非バーチャル バス入力をバーチャル バス入力に変換する実装で置き換えるルール。この実装にはテスト オブジェクティブが含まれ、最初と 3 番目の入力端子の値が異なる場合、それぞれのスイッチ位置を確認する必要があります。

blkrep_rule_selector
IndexVecPort_normal.m

Test Condition ブロックまたは Proof Assumption ブロックを、[インデックス オプション] パラメーターが Index vector (port)Selector ブロックのインデックス端子に追加するルール。Test Condition ブロックまたは Proof Assumption ブロックは信号値を、Selector ブロックの [入力の端子サイズ] および [インデックス モード] パラメーターの値から導出されたエンドポイントの間隔に制約します。

blkrep_rule_selector
StartingIdxPort_normal.m

Test Condition ブロックまたは Proof Assumption ブロックを、[インデックス オプション] パラメーターが Starting index (port)Selector ブロックのインデックス端子に追加するルール。Test Condition ブロックまたは Proof Assumption ブロックは信号値を、Selector ブロックの [入力の端子サイズ][出力サイズ] および [インデックス モード] パラメーターの値から導出されたエンドポイントの間隔に制約します。

ブロック置換ルールのテンプレート

ブロック置換ルールを作成しやすくするために、Simulink Design Verifier では必須コールバックのスケルトン実装を含む注釈付きテンプレートが提供されています。

matlabroot/toolbox/sldv/sldv/sldvblockreplacetemplate.m

ブロック置換ルールを作成するには、テンプレートをコピーし、そのコピーを編集して、作成するルールに要求する動作を実装します。テンプレートのコメントには、各セクションの使い方に関するヒントが示されています。

ブロック置換ルールには以下の制限があります。

  • ブロック置換ルールを表す関数には特定のコールバックが含まれていなければなりません。カスタム ルール記述には、まずブロック置換ルールのテンプレートを使用します。(Replace Unsupported Blocks Using Block Replacementsを参照してください。)

  • ブロック置換ルールを表す関数は、MATLAB® 検索パス上になければなりません。

ブロック置換によるテスト生成への影響

置換されるブロックがモデルの他の部分と機能を共有している場合、ブロック置換がテスト ケースの生成に影響する可能性があります。ブロックの置換は、これらのブロックや共有される信号との機能の依存関係を理解した上で行ってください。詳細については、機能の依存関係の強調表示を参照してください。代替ブロックはプロパティ証明など、他の解析のワークフローにも影響する可能性があります。

たとえば、入力信号にオブジェクティブを追加するブ代替ブロックを使用して、ブロックを解析向けにカスタマイズできます。他のサブシステムがその信号に依存している場合、代替ブロックはそのサブシステムのオブジェクティブを効率的に追加します。

この例では、2-D Lookup Table の u1 のブレークポイントの範囲は 5–7 です。切り替えしきい値 8 はルックアップ テーブルの範囲 u1 から外れます。

Simulink model with a switch block and a 2-D Lookup Table block.

2-D Lookup Table を置換せずに生成されたテストは、2 つのオブジェクティブを達成します。つまり、トリガーが Switch ブロックのしきい値 8 以下である場合と、Switch ブロックのしきい値 8 より大きい場合です。

達成されたオブジェクティブ

Table showing satisfied objective status.

blkrep_rule_lookup2D_normal.m ブロック置換ルールは 2-D Lookup Table を 2-D Lookup Table と MATLAB Function ブロックを含むマスク サブシステムに置換します。

Simulink model having Verification Subsystem and 2-D Lookup Table block.

MATLAB Function ブロックは解析をテーブルが示すブレークポイントの範囲内に制約します。

参考

トピック