Main Content

このページの翻訳は最新ではありません。ここをクリックして、英語の最新版を参照してください。

近似

モデル解析時の近似

Simulink® Design Verifier™ ソフトウェアは、複数の入力およびパラメーターの生成を行うことでオブジェクティブを達成しようとします。しかし、無数の値がその検索の対象になる可能性があります。解析に適切な制限を設けるために、解析を単純化する近似を実行します。実行された近似はすべて Simulink Design Verifier HTML レポートの解析情報の章に記録されます。この章の詳細は、解析情報の章を参照してください。

近似が行われている場合、解析結果のレビューは慎重に行ってください。モデルを評価して、近似の実施要因となったブロックまたはサブシステムを特定します。

まれに、近似の結果が、テスト オブジェクティブ達成や設計エラーの実例提示に失敗したテスト ケースになったり、証明オブジェクティブを反証できない反例になったりすることがあります。たとえば、しきい値を超えることでオブジェクティブを達成するテスト ケースの信号が生成されるとします。浮動小数点の丸め誤差によりその信号はしきい値に到達しない場合があります。

近似のタイプ

Simulink Design Verifier ソフトウェアはモデルの解析時に次の近似を行います。

浮動小数点から有理数への変換

場合によっては、Simulink Design Verifier ソフトウェアは浮動小数点数を無限精度の有理数で近似して、浮動小数点数の線形演算を単純化します。これにより、それらの値の間の論理的関係がオブジェクティブに与える影響が検出されます。この解析により、一般的に組み込み制御設計に見られる監視ロジックをこのソフトウェアでサポートすることが可能になります。

モデルの信号、入力値またはブロック パラメーターに浮動小数点値がある場合、Simulink Design Verifier は解析を実行する前に一部の値を有理数に変換します。これらの近似の結果は次のようになります。

  • 丸め誤差は考慮されません。

  • 浮動小数点数の上限と下限は考慮されません。

  • モデルが浮動小数点値を整数値にキャストする場合、このモデルに対して生成されたテストが整数表現の影響を受ける可能性があります。生成されたテストが、浮動小数点値に関連付けられているオブジェクティブを達成しないことがまれにあります。

浮動小数点データ型の 2 次元ルックアップ テーブルの線形化

Simulink Design Verifier ソフトウェアは、浮動小数点データ型の非線形演算をサポートしません。モデルに 2-D Lookup Table ブロック、あるいは以下のすべての特性をもつ、n = 2 の n-D Lookup Table ブロックが含まれる場合、平面を各内挿の間隔に相応させることで、非線形の 2 次元の内挿が線形内挿で近似されます。

ブロック特性

n-D Lookup Table ブロック、n = 2:

  • [内挿法] パラメーターが [線形] である。

  • [外挿法] パラメーターが [クリップ] または [線形] である。

  • 入力と出力の両方の信号が浮動小数点データ型をもつ。

整数と固定小数点データ型の 1 次元および 2 次元ルックアップ テーブルの近似

次の特性をもつルックアップ テーブルがモデルに含まれる場合、Simulink Design Verifier は、元のルックアップ テーブルを自動的に変換し、新しいルックアップ テーブルのブレークポイントが、それぞれの次元で等間隔になるように構成します。

ブロック特性

n-D Lookup Table ブロック、n = 1 または n = 2:

  • [内挿法] パラメーターが [線形] である。

  • [外挿法] パラメーターが [クリップ] である。

  • [インデックス検索法] パラメーターが [線形探索] または [二分探索] である。

  • 入力信号と出力信号がどちらも同じ型で、どちらも整数型または固定小数点型である。

この近似により Simulink Design Verifier でのテスト生成が非常に速くなります。節約される時間はモデル内に達成されないテスト オブジェクティブがある場合に顕著になります。

Simulink Design Verifier では、このような近似がモデルに適用される場合、Simulink Design Verifier レポートに近似の詳細が含まれます。

While ループ

モデルまたはモデル内の Stateflow® チャートに while ループが含まれる場合、Simulink Design Verifierwhile ループを終了できる保守的な定数境界を検出しようとします。定数境界が見つからない場合は、while ループの近似を行います。この近似により、解析ではオブジェクティブが有効であることも、達成されないことも証明せず、デッド ロジックも証明しません。生成された解析レポートにはこの近似について記されます。

while ループの近似の動作は、どの解析モードでも次の表に示されているとおりになります。

解析モードWhile ループの近似
設計エラー検出while ループの反復回数を 3 に設定します。デッド ロジックまたは有効なオブジェクティブをレポートしません。
テスト ケースの生成while ループの反復回数を 3 に設定します。達成されないオブジェクティブをレポートしません。
プロパティ証明while ループの反復回数を 3 に設定します。有効なオブジェクティブをレポートしません。