大規模で複雑なモデルの解析の実行
Simulink® モデルのいくつかの特性により、Simulink Design Verifier™ 解析で問題が発生する場合があります。これには、次が含まれます。
大量の入力、入力のタイプ、モデル状態および解析のオブジェクティブへの入力の影響の与え方が原因で生じるモデル入力の複雑化
モデル全体であり得るシミュレーション パスの数
到達不可能なモデルの部分
モデル内の大きなカウンター
これに加え、Simulink Design Verifier ソフトウェアでは、大規模モデルを解析する際に次のような問題が発生する場合があります。
オブジェクティブが達成されない — これらのテスト オブジェクティブを確認するテスト ケースがないことが証明され、テスト ケースが生成されませんでした。
オブジェクティブが判定不能 — これらのオブジェクティブを達成させる、あるいは反証することができませんでした。
エラーを含むオブジェクティブ — この問題は通常、モデルのコンポーネントが非線形演算を使用している場合に発生します。これはテスト オブジェクティブに影響することがあります。
割り当てられた時間内に解析を完了できない — この問題は、ソフトウェアに問題が発生したモデルの領域を示している可能性があります。また、[最大解析時間] パラメーターの値を大きくしなければならない場合があります。
解析がハングする — 処理されるオブジェクティブの数がかなり長い時間一定である場合、モデルとそのオブジェクティブの間で複雑な状況が発生している可能性があります。
モデル カバレッジで高いパーセンテージを達成できない — ハーネス モデルでテスト ケースを実行したときに、設計に対するモデル カバレッジのパーセンテージが不十分な場合に発生します。
大規模でより複雑なモデルでは、Simulink Design Verifier は、目的のオブジェクティブに影響しないモデルの部分を特定したり、検索の複雑度を低減させるモデル内の関係を検出したり、あるオブジェクティブの中間結果を別のオブジェクティブで再利用したりすることで、数学的手法により解析を簡略化します。このようにして、問題はモデルを記述する論理値による 1 つの検索にまで絞り込まれます。大規模モデルの解析の詳細は、大規模で複雑なモデルの解析の実行を参照してください。
Simulink Design Verifier で大規模モデルの解析を簡略化する方法
大規模で複雑なモデルでは、Simulink Design Verifier は次の数学的手法により解析を簡略化します。
目的のオブジェクティブに影響しないモデルの部分を特定します。
検索の複雑度を低減させるモデル内の関係を検出します。
あるオブジェクティブの中間結果を別のオブジェクティブで再利用します。
このようにして、問題はモデルを記述する論理値による 1 つの検索にまで絞り込まれます。
次のいくつかの節で、大規模モデルを解析する際に行う最初の手順について説明します。これらの手法の多くは、大規模モデル用のテスト生成を中心とするもので、モデルの複雑度の低減に使用されます。とはいえ、その多くは設計エラーの検出や大規模モデルのプロパティの証明に、また反証されたプロパティがあれば反例の作成に利用できます。
テスト生成アドバイザーを使用したモデルの階層構造と互換性の概要作成
テスト生成アドバイザーを使用して、モデルとモデル コンポーネントについてテスト生成の互換性、条件と判定オブジェクティブおよびデッド ロジックについての概要を作成できます。
テスト生成アドバイザーは高水準の解析およびデッド ロジックの高速検出を実行します。この結果を使用して、モデルをよりよく理解することができます。これは、大規模なモデルや複雑なモデル、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
未判定またはエラーが含まれるオブジェクティブをもつモデル要素をレビューして、次の問題が存在するかどうかを確かめます。"参照先" 列に示されているページを参照して、解析を改善するための手法を調べます。
モデルの問題 回避方法 浮動小数点の入力または非線形演算
既定では、Simulink Design Verifier はデータ型を double として解釈する場合があり、これによって解析中に精度の問題が生じる可能性があります。解析の精度を向上させるには、既知の場合はデータ型を明示的に指定し、可能な限りデータ型を単純化します。タイマーとカウンターには整数データ型を使用し、不要なキャスト演算子を避けて非線形演算を削減します。モデル入力の最小値と最大値を設定するか、Test Condition ブロックまたは sldv.assume ブロックを使用して入力範囲または信号範囲を離散化することで、データ型範囲を制約します。詳細については、モデル データ管理による解析の単純化および論理演算のショートサーキットを参照してください。 大規模な状態空間
遅延する入力信号に制約を適用する。
条件に基づいて実行されるサブシステムの中に含まれる状態に入力を制約する。
[最大テスト ケース ステップ数] パラメーターを
20に設定して、テスト ケース ステップ数を制限する。モデルの一部またはすべてのサンプル時間を増やす (この手順は、カウンターとタイマーで説明されているタイマーのしきい値を小さくする方法に似ています)。低いサンプルレートで生成されるテスト ケースは、多くの場合、オブジェクティブを達成する必要がある高いサンプルレートのテスト ケースと似ています。
極力厳密な変数の型を使用する。たとえば、値が 0 または 1 しかないフラグが
doubleで定義されている場合、この型をBooleanに制限します。
また、既存のシミュレーション データを使用して、テストの要件を満たすために役立てることもできます。既存のテスト データがある場合、それをモデル上で実行してモデル カバレッジを収集します。既存のテスト スイートを拡張して未達モデル カバレッジを達成する例については、既存テスト スイートの拡張を参照してください。モデル解析のボトムアップ アプローチも参照してください。
大きなタイマーおよび時間遅延
カウンターとタイマーおよびモデル解析のボトムアップ アプローチに記載されている回避方法を使用します。
解析レポート生成に割り当てるメモリ サイズの引き上げ
ルートレベルで大きな入力信号カウントをもつモデルを解析する場合、Simulink Design Verifier によるレポート生成時にメモリ不足エラーが発生することがあります。
これが発生する場合は、Sun® Java® 仮想マシン (JVM®) ソフトウェアが割り当て可能なメモリ量を増やす必要があります。このメモリを増加させる方法の手順は、MATLAB JVM メモリ割り当て制限を増やす (MATLAB Report Generator)を参照してください。
参考
モデル解析のボトムアップ アプローチ | カウンターとタイマー | モデル データ管理による解析の単純化
