Main Content

Simulink Design Verifier の改良条件判定カバレッジ

Simulink® Coverage™ カバレッジの記録に適用される設定に応じて、Simulink Coverage のモデル カバレッジ解析で使用される改良条件判定カバレッジ (MCDC) の定義と Simulink Design Verifier™ のテスト ケース生成解析で使用される定義とでは、違いが生じることがあります。

Simulink Coverage と Simulink Design Verifier の MCDC 定義

Simulink Design Verifier と Simulink Coverage は、MCDC オブジェクティブを 2 つの異なる方法で表します。

  • Simulink Coverage は論理式のそれぞれの条件を MCDC オブジェクティブとして取り扱います。

  • Simulink Design Verifier は、それぞれの独立ペアの true と false の分を個別の MCDC オブジェクティブとして扱います。

Simulink Design Verifier の [結果] ウィンドウには、正当化済み MCDC オブジェクティブについて [正当化済み] が表示されます。対応する [表示] リンクをクリックすると、Simulink Design Verifier の [解析フィルター] ウィンドウにフィルターの規則が表示されます。

非達成、または未判定の MCDC オブジェクティブには [正当化] のリンクが含まれます。このリンクをクリックすると、対応するフィルターの規則が作成されます。Simulink Coverage のすべての MCDC オブジェクティブが Simulink Design Verifier の 2 つの MCDC オブジェクティブに対応するため、Simulink Design Verifier の MCDC オブジェクティブはペアで正当化されます。

たとえば、次の図で、MCDC の式 expression for output with input port 4 false の [正当化] リンクをクリックすると、この MCDC オブジェクティブと、式が true の場合の MCDC オブジェクティブを正当化するフィルターの規則が作成されます。

On the left, the Simulink Design Verifier Results window shows results for the model analyzed. On the right, the Analysis Filter window shows justified MCDC outcomes and their rationales.

Simulink Design Verifier では、テスト ケース生成にマスキング MCDC 定義を常に使用します。既定では、Simulink Coverage でも、カバレッジを記録する際にマスキング MCDC 定義を使用します。しかし、CovMcdcMode モデル コンフィギュレーション パラメーターを 'UniqueCause' に設定すると、Simulink Coverage ではカバレッジを記録する際にユニークコーズ MCDC 定義が代わりに使用されます。マスキング MCDC 定義とユニークコーズ MCDC 定義の違いの詳細については、Simulink Coverage における改良条件判定カバレッジ (MCDC) 定義を参照してください。

CovMcdcMode モデル コンフィギュレーション パラメーターを 'UniqueCause' に設定すると、Simulink Coverage の MCDC レポートと Simulink Design Verifier のテスト生成の間に違いが生ずることがあります。この違いの例は、以下の Stateflow® 遷移にあるような、演算子 AND と OR の組み合わせによる論理式に対する解析結果で見ることができます。

Stateflow transition 1 condition [(A && B) || C] that sets {out = 1;}. Transition 2 does not have a condition and sets {out = 0;}.

A、B および C がそれぞれ独立した入力として与えられる場合、Stateflow 遷移条件の評価方法は次の表が示すように、5 通り考えられます。

 ABC(A && B) || C
1FxFF
2FxTT
3TFFF
4TFTT
5TTxT

論理変数の MCDC を達成させるには、条件のペアが評価されることが必要です。その変数の 1 つの変更だけで、式全体の評価が変化することになります。この例では、1 と 2 または 3 と 4 のいずれかのペアで C の MCDC を達成させることができます。どちらの場合も、C の値が変わるため式の値が変化しますが、その他のすべての変数値は同じままです。

それぞれのペアには、A と B の異なる値のセットがあり、それらは一定に保たれますが、C と out が true となる 1 つの評価と C と out が false となる 1 つの評価が含まれます。C の MCDC を達成させるには、Simulink Design Verifier テスト生成解析で C と out の 1 つの true 値の評価と 1 つの false 値の評価を含む任意のペアを受け入れます。この例では、Simulink Design Verifier のテスト生成解析によって、1 と 2 のペアおよび 3 と 4 のペアのみでなく、1 と 4 のペアおよび 2 と 3 のペアも受け入れられています。ユニークコーズ MCDC 定義を使用する Simulink Coverage モデル カバレッジ解析は、1 と 2 のペアまたは 3 と 4 のペアによってのみ達成されます。

前の例では、A、B および C はすべて独立した入力と想定されます。このモデルのように入力 A が C と同じ値になるように制約される場合、条件評価のサブセットのみが使用できます。

次の表は、この Stateflow 遷移の条件評価のサブセットを示します。

 ABC(A && B) || C
1FxFF
4TFTT
5TTxT

評価 2 と 3 は使用できなくなるので、1 と 2 および 3 と 4 のペアも使用できなくなります。そのため、C のユニークコーズ MCDC は Simulink Coverage モデル カバレッジ解析で達成されなくなります。ただし、1 と 4 のペアは使用可能なままなので、Simulink Design Verifier テスト生成解析では C の MCDC は達成されるとレポートされます。

AND と OR 演算子が組み合わされた論理式に対する MCDC 解析の複雑性は、ユニークコーズ MCDC 解析が設定された Simulink Coverage と Simulink Design Verifier の結果において、この差が発生する原因となります。CovMcdcMode モデル コンフィギュレーション パラメーターの既定値である 'Masking' では、この相違は生じません。ただし、Simulink Coverage でユニークコーズ MCDC 解析の使用が必要な場合は、Simulink Design Verifier のテスト生成解析で [IndividualObjectives] テスト スイート最適化を使用すると、この影響を最小限に抑えることができます。詳細については、テスト スイートの最適化 (Simulink Design Verifier)の「ヒント」節を参照してください。

関連するトピック

  • MCDC (Simulink Design Verifier)