大規模モデルの解析

大規模モデルの問題のタイプ

Simulink^® Design Verifier™ ソフトウェアでは、大規模モデルを解析する際に次のような問題が発生する場合があります。

オブジェクティブが達成されない — これらのテストオブジェクティブを確認するテストケースがないことが証明され、テストケースが生成されませんでした。
オブジェクティブが判定不能 — これらのオブジェクティブを達成させる、あるいは反証することができませんでした。
エラーを含むオブジェクティブ — この問題は通常、モデルのコンポーネントが非線形演算を使用している場合に発生します。これはテストオブジェクティブに影響することがあります。
割り当てられた時間内に解析を完了できない — この問題は、ソフトウェアに問題が発生したモデルの領域を示している可能性があります。また、[最大解析時間] パラメーターの値を大きくしなければならない場合があります。
解析がハングする — 処理されるオブジェクティブの数がかなり長い時間一定である場合、モデルとそのオブジェクティブの間で複雑な状況が発生している可能性があります。
モデルカバレッジで高いパーセンテージを達成できない — ハーネスモデルでテストケースを実行したときに、設計に対するモデルカバレッジのパーセンテージが不十分な場合に発生します。

次のいくつかの節で、大規模モデルを解析する際に行う最初の手順について説明します。これらの手順ではテスト生成を取り扱いますが、設計エラーを検出する場合またはモデルのプロパティを証明する場合も同様の方法を使用できます。

モデルの階層構造と互換性の概要

テスト生成アドバイザーを使用して、モデルとモデルコンポーネントについてテスト生成の互換性、条件と判定オブジェクティブおよびデッドロジックについての概要を作成できます。

テスト生成アドバイザーは高水準の解析およびデッドロジックの高速検出を実行します。この結果を使用して、モデルをよりよく理解することができます。これは、大規模なモデルや複雑なモデル、Simulink Design Verifier との互換性が確実に把握できていないモデルで特に便利です。たとえば、次のようなことができます。

テストケース生成との非互換性の特定
解析に時間がかかる可能性のある複雑なコンポーネントの特定
デッドロジックのインスタンスの特定
コンポーネント階層の概要の取得
推奨されるテスト生成パラメーターの取得

テスト生成アドバイザーにアクセスするには、[Design Verifier] タブの [モード] セクションで [テスト生成] をクリックします。[準備] セクションで [アドバイザー] をクリックします。詳細は、テスト生成アドバイザーによる解析可能コンポーネントの特定を参照してください。

既定のパラメーター値の使用

一般にテストケースを生成するときは、まず Simulink Design Verifier の既定のパラメーター値を使用してモデルの解析を始めてください。

モデルの互換性チェックで説明されているように、モデルが Simulink Design Verifier と互換であるかどうかをチェックします。

既定のパラメーター値を使用して、モデルを解析します。次の表は、大規模モデルの解析時に変更される可能性のある [コンフィギュレーションパラメーター] ダイアログボックスのパラメーターの既定値の一覧です。

パラメーター	既定値	説明
最大解析時間 (秒)	`300` (秒)	指定された時間内に解析が終了しない場合、解析はタイムアウトになり終了します。
テストスイートの最適化	`Auto`	複数のテストオブジェクティブを処理するテストケースを生成します。
モデルカバレッジオブジェクティブ	`条件判定`	条件および判定カバレッジを達成するテストケースを生成します。

解析の実行時に、Simulink Design Verifier のログウィンドウで次の情報をレビューします。
- 処理されたオブジェクティブの数 — いくつのオブジェクティブが処理されたか。一定数のオブジェクティブの処理後に解析がハングしたか。これらの問いの答えが問題の所在に関するヒントになることがあります。
- 達成されたオブジェクティブ数/反証されたオブジェクティブ数 — どのオブジェクティブが反証されたか。
- 経過時間 — 解析がタイムアウトしたか、または指定された最大解析時間内に終了したか。
モデルにおける結果の強調表示で説明されているように、解析が完了したときに、モデルの結果を強調表示して各モデルオブジェクトの解析を個別にレビューすることができます。また、Simulink Design Verifier HTML レポートを生成してレビューすることもできます。このレポートには達成されたオブジェクティブおよび反証されたオブジェクティブのモデル要素へのリンクが含まれ、モデル内で問題の可能性がある部分を確認することができます。詳細は、結果の確認を参照してください。
テスト生成解析では、すべてのテストオブジェクティブが達成されている場合、ハーネスモデルのテストケースを実行して、モデルカバレッジを判定します。
設計に対してモデルカバレッジが十分であれば、他に何もする必要はありません。カバレッジが不十分であれば、解析性能を向上させるため、次の節で説明するように追加の手順を行います。

メモ

反証されたオブジェクティブの割合が高く、モデルカバレッジが乏しいということは、たいていの場合、フルカバレッジを得るためにはモデルパラメーター値の変更が必要であることを意味します。これは、Switch ブロック内の有効なサブシステムまたはトリガー入力に接続されている Constant ブロックに調整可能なパラメーターがある場合に発生する可能性があります。このような状況では、Specify Parameter Configuration for Full Coverageの例で説明されているように、Simulink Design Verifier のパラメーターのサポートを構成します。

解析パラメーターの変更

解析でごく一部のオブジェクティブのみが達成されなかった場合は、次の手順を試します。

[最大解析時間] パラメーターを大きくします。これにより、すべてのオブジェクティブを達成させるための解析時間が長くなります。
[モデルカバレッジオブジェクティブ] パラメーターを [判定] に設定します。このオプションを選択すると、判定カバレッジを達成するテストケースのみが生成されます。これらのテストケースは、MCDC オプションのサブセットです。
解析を再実行してレポートをレビューします。
結果が依然として不十分である場合、次の節で説明されている手法を試してください。

解析の完了前の停止

ログウィンドウで [処理されたオブジェクティブ] の値を監視します。[最大解析時間] パラメーターの 50% 程度が経過してもこの値が増加しない場合、モデルの解析でなんらかのオブジェクティブの処理中に問題が発生している可能性があります。解析が進まない場合、以下の手順を行います。

ログウィンドウで [停止] をクリックします。
ダイアログボックスが開き、解析が中断されたことが示され、引き続き結果を生成するかどうかを尋ねられます。
[はい] をクリックして、その時点の解析結果を保存します。
ログウィンドウには、実行した解析モードに応じて、次のオプションがリストされます。
- 解析結果をモデル上で強調表示
- 詳細な解析レポートを生成
- ハーネスモデルの作成
- テストをシミュレートしてモデルカバレッジレポートを生成
[詳細な解析レポートを生成] をクリックします。
HTML レポートで、次の節をレビューして問題の原因となるモデル要素を特定します。
- Objectives Undecided when the Analysis was Stopped
- Objectives Producing Errors

未判定またはエラーが含まれるオブジェクティブをもつモデル要素をレビューして、次の問題が存在するかどうかを確かめます。"参照先" 列に示されているページを参照して、解析を改善するための手法を調べます。

モデルの問題	参照先
浮動小数点の入力	モデルデータ管理による解析の単純化モデル解析のボトムアップアプローチ
非線形操作	論理演算モデル解析のボトムアップアプローチ
大規模な状態空間	大規模な検証状態空間をもつモデルの解析モデル解析のボトムアップアプローチ
大きなタイマーおよび時間遅延	カウンターとタイマーモデル解析のボトムアップアプローチ