タereplicationトル

タ@ @トル節には次の情報がリストされます。

目次

目次がタ@ @トルに続きます。目次の項目をクリックすると、レポートのそれぞれの章にすばやく移動できます。

モデル情報

モデル情報の節では，モデルの現在のバ，ジョンに関する次の情報が提供されます。

解析オプション

解析オプションの節では万博1manbetxSimulink设计验证器解析の設定に関する情報が提供されます。

解析オプションの節には，万博1manbetxSimulink设计验证器解析に影響を及ぼしたパラメ，タ，がリストされます。カバレッジフィルタ処理を有効にした場合，そのフィルタファル名がこの節に記載されます。

サポ，トされていないブロック

モデルにサポートされないブロックが含まれる場合,既定で有効化されている自動スタブにより,解析は続行されます。自動スタブが有効な場合,サポートされないブロックのインターフェイスのみが考慮され,実際の動作は考慮されません。この手法により解析の完了が可能になります。ただし,サポートされないモデルブロックのいずれかがシミュレーションの結果に影響するものである場合,部分的な解析結果しか得られない可能性があります。

サポートされていないブロックの節は,解析でサポートされていないブロックがスタブされた場合にのみ表示されます。ここでは,サポートされていないブロックが,モデル内の各ブロックへのハイパーリンクとともに,表にリストされます。

自動スタブの詳細は，自動スタブによる非互換性処理を参照してください。

ユ，ザ，ア，ティファクト

ユ，ザ，ア，ティファクトの節には，万博1manbetxSimulink设计验证器の解析のテストデ，タとカバレッジデ，タに関する情報が示されます。

制約

制約の節には，万博1manbetxSimulink设计验证器がモデルを解析したときに適用したテスト条件に関する情報が示されます。

制約の表のハ。モデルウィンドウ内の対応する测试条件ブロックが強調表示され,新しいウィンドウが開いてブロックの詳細が表示されます。

ブロック置換の概要

ブロック置換の概要には，万博1manbetxSimulink设计验证器が実行したブロック置換の概要が示されます。これは，万博1manbetxSimulink设计验证器がモデル内でブロックを置き換えた場合にのみ表示されます。

表の各行は，万博1manbetxSimulink设计验证器がモデルに適用した個々のブロック置換ル，ルに対応します。表には以下がリストされます。

モデルの特定のブロック置換を見つけるには,表の替换块列にあるその置換名をクリックします。適用されたブロックがモデルウィンドウで強調表示され,新しいウィンドウが開いてブロックの詳細が表示されます。

近似

近似の表の各行には，万博1manbetxSimulink设计验证器がモデルの解析中に使用した近似のタ@ @プがそれぞれ示されています。

解析のハ，ネス情報

[解析のハ，ネス情報]節には，モデルの解析に使用される万博1manbetxSimulink设计验证器によって生成された解析ハ，ネスの概要が示されます。[解析のハ，ネス情報]節には，モデルがエクスポ，ト関数モデルか，対応するS万博1manbetximulink関数をもたない函数调用者ブロックを含むモデルかに基づいて，次の小節が表示されます。

エクスポ，ト関数解析のスケジュ，ル。万博1manbetxSimulink设计验证器は，解析時に导出功能を呼び出すための解析ハ，ネスを想定します。たとえば，次の表は，モデルsldvExportFunction_autosar_multirunnablesの解析ハ，ネスを示しています。

解析用にスタブされたS万博1manbetximulink関数。[解析用にスタブされたS万博1manbetximulink関数]の次の表は,解析ハーネスでスタブされた仿万博1manbetx真软件関数に対応する関数プロトタイプを示しています。

設計エラ，検出オブジェクティブのステ，タス

設計エラ，検出解析を実行すると，[設計エラ，検出オブジェクティブのステ，タス]節には次のオブジェクティブステ，タスが記載されます。

• デッドロジック

• 近似におけるデッドロジック

• アクティブロジック-シミュレションが必要

• 有効なオブジェクティブ

• 近似において有効なオブジェクティブ

• 反例によって反証されたオブジェクティブ

• 反証されたオブジェクティブ-シミュレションが必要

設計エラ，検出解析で观察者参考ブロックが使用されている場合，この節では，オブザ，バ，の情報が[オブザ，バ，モデル]小節に，設計モデルの情報が[設計モデル]小節にそれぞれ表示されます。モデル内にアクティブロジックが存在しない場合，この節は空になります。

[設計モデル]小節の表は，モデル例sldvdemo_debounce_validpropのアクティブロジックのリストを示しています。

オブザーバーは設計エラー検出解析で無視されるため,[オブザーバーモデル]節には,レポートされているアクティブロジックが表示されません。

デッドロジック。[デッドロジック]節には，解析でデッドロジックが見かった項目がリストされます。

次の図は，sldvdemo_fuelsys_logic_simpleモデルで生成された解析レポ，トの[デッドロジック]節を示しています。

近似におけるデッドロジック。[近似におけるデッドロジック]節には，解析で近似の影響を受けるデッドロジックが見かったモデルの項目がリストされます。

R2017bより前のリリ、スでは、この節には[デッドロジック]としてマ，クされているオブジェクティブが含まれる場合があります。

次の図は，生成された解析レポ，トの[近似におけるデッドロジック]節を示しています。

アクティブロジック-シミュレションが必要。[アクティブロジック-シミュレションが必要]節には，解析でアクティブロジックが見かったモデルの項目がリストされます。アクティブロジックのステータスを確認するには,テストケースのシミュレーションを追加で実行しなければなりません。

R2017bより前のリリ、スでは、この節には[アクティブロジック]としてマ，クされているオブジェクティブが含まれる場合があります。

次の図は，sldvdemo_fuelsys_logic_simpleモデルで生成された解析レポ，トの[アクティブロジック-シミュレションが必要]節の一部を示しています。

有効なオブジェクティブ。[有効なオブジェクティブ]節には，解析で有効であることがわかった設計エラ，検出オブジェクティブがリストされます。これらのオブジェクティブについては,解析によって,記述された設計エラーは発生することがないと判断されています。

R2017bより前のリリ、スでは、この節には[有効であると証明済み]とマ，クされているオブジェクティブが含まれる場合があります。

次の図は，sldvdemo_design_error_detectionモデルで生成された解析レポ，トの[有効なオブジェクティブ]節を示しています。

近似において有効なオブジェクティブ。[近似において有効なオブジェクティブ]節には,解析で近似の影響の下で有効であることがわかった設計エラー検出オブジェクティブがリストされます。

R2017bより前のリリ、スでは、この節には[有効であると証明済み]とマ，クされているオブジェクティブが含まれる場合があります。

次の図は，生成された解析レポ，トの[近似において有効なオブジェクティブ]節を示しています。

反例によって反証されたオブジェクティブ。[反例によって反証されたオブジェクティブ]には,報告されたエラーを確認するために反例がシミュレートされ検証された設計エラー検出オブジェクトのセットがリストされます。

次の図は，sldvdemo_design_error_detectionモデルで生成された解析レポ，トの[反例によって反証されたオブジェクティブ]節を示しています。

反証されたオブジェクティブ-シミュレションが必要。[反証されたオブジェクティブ-シミュレションが必要]節では,設計エラーを示すテストケースが解析で見つかった設計エラー検出オブジェクティブがリストされます。反証ステ，タスを確認するには，テストケ，スのシミュレ，ションを追加で実行しなければなりません。

R2017bより前のリリ、スでは、この節には[反証]とマ，クされているオブジェクティブが含まれる場合があります。

次の図は，sldvdemo_array_boundsモデルで生成された解析レポ，トの[反証されたオブジェクティブ-シミュレションが必要]節を示しています。

テストオブジェクティブのステ，タス

テストケ，ス生成解析を実行すると，[テストオブジェクティブのステ，タス]節には次のオブジェクティブステ，タスが記載されます。

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

• 達成されたオブジェクティブ-シミュレションが必要

• 達成されないオブジェクティブ

• 近似において非達成のオブジェクティブ

• テストケ，スで未判定のオブジェクティブ

[モデルカバレッジオブジェクティブ]を(增强MCDC)に設定してモデルを解析すると，ソフトウェアはモデル項目の検出ステ，タスをレポ，トします。詳細にいては，万博1manbetxSimulink设计验证器の拡張MCDCカバレッジを参照してください。

テストケ，ス生成解析で观察者参考ブロックが使用されている場合，各テストオブジェクティブステ，タス節では，オブザ，バ，の情報が[オブザ，バ，モデル]小節に，設計モデルの情報が[設計モデル]小節にそれぞれ表示されます。モデル内にテストオブジェクティブが見からない場合，これらの小節は空になります。

この表は，モデル例sldvdemo_debounce_testobjblksにある設計モデルの[達成されたオブジェクティブ]のテストオブジェクティブの一部を示しています。

この表は，モデル例sldvdemo_debounce_testobjblksにあるオブザ，バ，モデルの[達成されたオブジェクティブ]のテストオブジェクティブの一部を示しています。

達成されたオブジェクティブ。[達成されたオブジェクティブ]節には，解析で達成されたテストオブジェクティブがリストされます。生成されたテストケ，スはオブジェクティブをカバ，します。

次の図は，モデル例sldvdemo_fuelsys_logic_simpleで生成された解析レポ，トの[達成されたオブジェクティブ]節の一部を示しています。

達成されたオブジェクティブ-シミュレションが必要。[達成されたオブジェクティブ-シミュレションが必要]節には，解析で達成されたテストオブジェクティブがリストされます。達成ステ，タスを確認するには，テストケ，スのシミュレ，ションを追加で実行しなければなりません。

R2017bより前のリリ、スでは、この節には[達成]としてマ，クされているオブジェクティブが含まれる場合があります。

次の図は，生成された解析レポ，トの[達成されたオブジェクティブ-シミュレションが必要]節を示しています。

達成されないオブジェクティブ。[非達成のオブジェクティブ]節には，解析で達成されないと判断されたテストオブジェクティブがリストされます。

R2017bより前のリリ、スでは、この節には[非達成と証明]とマ，クされているオブジェクティブが含まれる場合があります。

次の図は，モデル例sldvdemo_fuelsys_logic_simpleで生成された解析レポ，トの[非達成のオブジェクティブ]節を示しています。

近似において非達成のオブジェクティブ。[近似において非達成のオブジェクティブ]節には,解析時の近似により,解析で達成されないと判断されたテストオブジェクティブがリストされます。

R2017bより前のリリ、スでは、この節には[非達成と証明]とマ，クされているオブジェクティブが含まれる場合があります。

次の図は，生成された解析レポ，トの[近似において非達成のオブジェクティブ]節を示しています。

テストケ，スで未判定のオブジェクティブ。[テストケ，スで未判定のオブジェクティブ]節には，解析時の近似の影響により未判定のテストオブジェクティブがリストされます。

R2017bより前のリリ、スでは、この節には[達成]としてマ，クされているオブジェクティブが含まれる場合があります。

次の図は，モデル例sldvApproximationsExampleで生成された解析レポ，トの[テストケ，スで未判定のオブジェクティブ]節を示しています。

証明オブジェクティブステ，タス

プロパティ証明解析を実行すると，[証明オブジェクティブステ，タス]節には以下が記載されます。

• 有効なオブジェクティブ

• 近似において有効なオブジェクティブ

• 反例によって反証されたオブジェクティブ

• 反証されたオブジェクティブ-シミュレションが必要

• 反例で未判定のオブジェクティブ

プロパティ証明解析で观察者参考ブロックが使用されている場合，各証明オブジェクティブステ，タス節では，オブザ，バ，の情報が[オブザ，バ，モデル]小節に，設計モデルの情報が[設計モデル]小節にそれぞれ表示されます。モデル内にオブジェクティブが見からない場合，これらの小節は空になります。

この表は，モデル例sldvdemo_debounce_validpropにあるオブザ，バ，モデルの[有効なオブジェクティブ]の証明オブジェクティブを示しています。

有効なオブジェクティブ。[有効なオブジェクティブ]節には，解析で有効であることがわかった証明オブジェクティブがリストされます。

R2017bより前のリリ、スでは、この節には[有効であると証明済み]とマ，クされているオブジェクティブが含まれる場合があります。

次の図は，モデル例sldvdemo_debounce_validpropで生成された解析レポ，トの[有効なオブジェクティブ]節を示しています。

近似において有効なオブジェクティブ。[近似において有効なオブジェクティブ]節には，解析で近似の影響の下で有効であることがわかった証明オブジェクティブがリストされます。

R2017bより前のリリ、スでは、この節には[有効と証明されたオブジェクティブ]とマ，クされているオブジェクティブが含まれる場合があります。

次の図は，生成された解析レポ，トの[近似において有効なオブジェクティブ]節を示しています。

反例によって反証されたオブジェクティブ。[反例によって反証されたオブジェクティブ]節には，解析で反証された証明オブジェクティブがリストされます。生成された反例は，証明オブジェクティブの違反を示します。

次の図は，モデル例sldvdemo_debounce_falsepropで生成された解析レポ，トの[反例によって反証されたオブジェクティブ]節を示しています。

反証されたオブジェクティブ-シミュレションが必要。[反証されたオブジェクティブ-シミュレションが必要]節には，解析で反証された証明オブジェクティブがリストされます。反証ステ，タスを確認するには，反例のシミュレ，ションを追加で実行しなければなりません。

R2017bより前のリリ、スでは、この節には[反例によって反証されたオブジェクティブ]とマ，クされているオブジェクティブが含まれる場合があります。

次の図は，生成された解析レポ，トの[反証されたオブジェクティブ-シミュレションが必要]節を示しています。

反例で未判定のオブジェクティブ。[反例で未判定のオブジェクティブ]節には，解析時の近似の影響により未判定の証明オブジェクティブがリストされます。

R2017bより前のリリ、スでは、この節には[反証]とマ，クされているオブジェクティブが含まれる場合があります。

次の図は，生成された解析レポ，トの[反例で未判定のオブジェクティブ]節を示しています。

実行時エラ，のため未判定のオブジェクティブ

証明オブジェクティブおよびテストオブジェクティブにいて，[実行時エラ，のため未判定のオブジェクティブ]節には，実行時エラ，のため解析時に未判定のオブジェクティブがリストされます。テストケ，スまたは反例のシミュレ，ション中に実行時エラ，が発生しました。

R2017bより前のリリ、スでは、この節には[反証]または[達成]とマ，クされているオブジェクティブが含まれる場合があります。

次の図は，生成された解析レポ，トの[実行時エラ，のため未判定のオブジェクティブ]節を示しています。

ゼロ除算のため未判定のオブジェクティブ

すべてのタ化学键プのオブジェクティブに化学键いて，[ゼロ除算のため未判定のオブジェクティブ]節には，関連するモデル項目のゼロ除算エラ，のため解析時に未判定のオブジェクティブがリストされます。モデルの解析を続ける前にゼロ除算エラ，を検出するには，整数オ，バ，フロ，およびゼロ除算エラ，の検出の手順に従ってください。

非線形性のため未判定のオブジェクティブ

すべてのタ化学键プのオブジェクティブに化学键いて，[非線形性のため未判定のオブジェクティブ]節には，非線形演算の計算が必要なために解析時に未判定のオブジェクティブがリストされます。万博1manbetxSimulink设计验证器では，非線形演算および非線形ロジックがサポ，トされていません。

スタブのため未判定のオブジェクティブ

すべてのタ化学键プのオブジェクティブに化学键いて，[スタブのため未判定のオブジェクティブ]節には，スタブのために解析時に未判定のオブジェクティブを含むモデル項目がリストされます。R2013bより前のリリ、スでは、これらのオブジェクティブには、[達成されたオブジェクティブ-テストケスなし]または[反証されたオブジェクティブ-反例なし]とマ，クされているオブジェクティブが含まれる場合があります。

配列が範囲外にあたるため未判定のオブジェクティブ

すべてのタ化学键プのオブジェクティブに化学键いて，[配列が範囲外にあたるため未判定のオブジェクティブ]節には,関連するモデル項目に範囲外の配列エラーがあるため解析時に未判定になったオブジェクティブがリストされます。モデルから範囲外の配列エラ，を検出するには，配列の範囲外へのアクセスエラ，の検出を参照してください。

未判定のオブジェクティブ

オブジェクティブのすべてのタ化学键プに化学键いて，[未判定のオブジェクティブ]の節では，割り当てられた時間内に解析が結果を判定できなかったオブジェクティブがリストされます。

次のプロパティ証明の例では、このソフトウェアが解析時間の制限([最大解析時間]パラメーターで指定)を超えているか,これらのオブジェクティブの処理の完了前にユーザーが解析を中断しています。

目次

設計エラ，の章には目次があります。目次の各項目は、個々の設計エラーに関する結果へのハイパーリンクになっています。

概要

概要節では以下がリストされます。

次の例では，sldvdemo_debounce_falsepropモデルが解析され，設計エラ，が検出されています。验证真实输出という名前の验证子系统の总和ブロックでオ，バ，フロ，エラ，が検出されています。

テストケ，ス

テストケース節には,テストケースが設計エラーのオブジェクティブを反証したタイムステップと対応する時間がリストされます。轮廓尺寸ブロック生の値は255であり，これによってオ，バ，フロ，エラ，が発生しました。

目次

テストケ，スの章には目次があります。目次の各項目は、個々のテスト ケースに関する情報へのハイパーリンクになっています。

概要

概要節では以下がリストされます。

オブジェクティブ

オブジェクティブの節には以下がリストされます。

生成された入力デ，タ

生成された入力データの節では,モデルの項目に関連付けられた各入力信号について,テストケースが個々のテストオブジェクティブを達成するタイムステップおよび対応する時間がリストされます。信号値がそれらのタイムステップの間変化しない場合,表にはタイムステップと時間が範囲としてリストされます。

期待される出力

[コンフィギュレションパラメタ]ダアログボックスの(设计验证器)、[結果]ペereplicationンで[期待される出力値を含める]を選択すると,レポートにそれぞれのテストケースの预期输出節が記載されます。この表には,モデルの項目に関連付けられたそれぞれの出力信号について,各タイムステップで想定される出力値がリストされます。

结合目标

[テストス苹果平台，苹果平台，苹果平台，トの最適化]オプションを(CombinedObjectives)に設定すると(既定),测试用例の章に個々の情報が多数のテストケースについて示されます。

长测试用例

[テストス苹果平台，苹果平台，苹果平台，トの最適化]オプションを(LongTestcases)に設定すると,レポートの测试用例の章にはより長いテストケースに関する,より少数の節が記載されます。

目次

プロパティの章には目次があります。目次の各項目は、反証された個々のプロパティに関する情報へのハイパーリンクになっています。

プロパティ証明解析で观察者参考ブロックが使用されている場合，各プロパティの章では，オブザ，バ，の情報が[オブザ，バ，モデル]小節に，設計モデルの情報が[設計モデル]小節にそれぞれ表示されます。モデル内にプロパティがない場合は空になります。

この表は，モデル例sldvdemo_debounce_validpropにあるオブザバモデルのプロパティの1を示しています。

概要

概要節では以下がリストされます。

次の例では，sldvdemo_cruise_control_verificationモデルが解析され，プロパティが証明されています。BrakeAssertionという名前の断言ブロックへの入力が非ゼロであることが，解析により証明されています。

反例

反例節には,反例がプロパティを反証したタイムステップと対応する時間がリストされます。この節には，そのタ。