Simulink Design Verifier のチェック
Simulink Design Verifier のチェックの概要
これらのチェックは、Simulink® Design Verifier™ の解析を行うためのモデルの準備に役立ちます。Simulink Design Verifier のチェックを実行すると、モデル アドバイザーは Simulink Design Verifier ライセンスをチェックアウトします。
モデル アドバイザーの詳細については、モデル アドバイザー チェックの実行とモデル アドバイザー チェック実行の自動化を参照してください。
Simulink Design Verifier との互換性チェック
チェック ID: mathworks.sldv.compatibility
Simulink Design Verifier の解析でサポートされていない要素を特定します。
説明
このチェックでは、モデルと Simulink Design Verifier との互換性を評価します。
結果と推奨アクション
条件 | 推奨アクション |
---|---|
非互換 | 次に示すサポートされていないソフトウェア機能または Simulink ブロックは、解析するモデルまたはモデル コンポーネント内で使用しないようにしてください。 |
部分的に互換 |
|
互換 | Simulink Design Verifier はモデルを解析できます。 |
参考
デッド ロジックの検出
チェック ID: mathworks.sldv.deadlogic
シミュレーション中にアクティブにならないロジックを特定します。
説明
このチェックは、シミュレーション中にアクティブにならないモデルの部分を特定します。
Simulink Design Verifier の設計エラー検出を使用すると、より詳しい解析を実行してデッド ロジックとアクティブ ロジックの両方を特定することができます。詳細は、不適切な値を原因とするデッド ロジックの検出を参照してください。
このチェックの推奨事項に従うと、組み込みアプリケーション用の MISRA C:2012 準拠コードと、CERT C 標準および CWE 標準に準拠するコードが生成される可能性が高くなります。
結果と推奨アクション
結果 | 推奨アクション |
---|---|
失敗。モデルに互換性がない | モデルの非互換性を解決します。以下を参照してください。
自動スタブによる非互換性処理も参照してください。 |
デッド ロジックがモデルで検出された | Simulink Design Verifier によって、これらの判定と条件結果は発生し得ず、モデルにおいてデッド ロジックであることが証明されました。デッド ロジックは、パラメーターに指定された制約や、入力ポートに指定された最小制約および最大制約の副作用である場合もあります。また、Simulink Design Verifier による近似が原因でデッド ロジックが発生することも稀にあります。この解析で判定されなかったオブジェクティブが存在する可能性があります。解析の結果を拡張するには、アクティブ ロジックも特定できる Simulink Design Verifier の設計エラー検出を使用してください。Simulink エディターから、[アプリ] 、 [Design Verifier] 、 [設定] を選択します。[コンフィギュレーション パラメーター] ウィンドウで、[Design Verifier] 、 [設計エラー検出] ペインから、[デッド ロジック (一部)] を選択するか、DVDetectDeadLogic および DVDetectActiveLogic を on に設定します。 |
デッド ロジックがモデルで検出されなかった | Simulink Design Verifier はモデル内でデッド ロジックを検出しませんでした。この解析で判定されなかったオブジェクティブが存在する可能性があります。解析の結果を拡張するには、アクティブ ロジックも特定できる Simulink Design Verifier の設計エラー検出を使用してください。Simulink エディターから、[アプリ] 、 [Design Verifier] 、 [設定] を選択します。[コンフィギュレーション パラメーター] ウィンドウで、[Design Verifier] 、 [設計エラー検出] ペインから、[デッド ロジック (一部)] を選択するか、DVDetectDeadLogic および DVDetectActiveLogic を on に設定します。 |
参考
MISRA C:2012: ルール 2.1
CERT C、MSC07-C
CWE、CWE-561
Secure Coding (Embedded Coder)
範囲外配列アクセスの検出
チェック ID: mathworks.sldv.arraybounds
配列のインデックスの範囲外にアクセスする操作を検出します
説明
このチェックは Simulink Design Verifier で、配列の範囲外へのアクセスを行うインスタンスを検出します。
このチェックの推奨事項に従うと、組み込みアプリケーション用の MISRA C:2012 準拠コードと、CERT C 標準、CWE 標準、ISO/IEC TS 17961 標準に準拠するコードが生成される可能性が高くなります。
結果と推奨アクション
結果 | 推奨アクション |
---|---|
失敗。モデルに互換性がない | モデルの非互換性を解決します。次を参照してください。
自動スタブによる非互換性処理も参照してください。 |
モデル内で配列の範囲外へのアクセスを検出 | 配列の範囲外へのアクセスの原因となる条件を表示するには、ハーネス モデルを作成します。ハーネスのシミュレーションを行うと、入力はエラーを再現します。モデル アドバイザー レポートで [テスト ケースを表示] をクリックします。 |
参考
MISRA C:2012: ルール 18.1
ISO/IEC TS 17961: 2013、invptr
CERT C、ARR30-C
CWE、CWE-118
Secure Coding (Embedded Coder)
ゼロ除算の検出
チェック ID: mathworks.sldv.divbyzero
モデル内のゼロ除算エラーを検出します
説明
このチェックは、ゼロ除算エラーの原因となるモデル内の演算を特定します。
このチェックの推奨事項に従うと、組み込みアプリケーション用の MISRA C:2012 準拠コードと、CERT C 標準、CWE 標準、ISO/IEC TS 17961 標準に準拠するコードが生成される可能性が高くなります。
結果と推奨アクション
結果 | 推奨アクション |
---|---|
失敗。モデルに互換性がない | モデルの非互換性を解決します。次を参照してください。
自動スタブによる非互換性処理も参照してください。 |
モデル内でゼロ除算を検出 | ゼロ除算の原因となる条件を表示するには、ハーネス モデルを作成します。ハーネスのシミュレーションを行うと、入力はエラーを再現します。モデル アドバイザー レポートで [テスト ケースを表示] をクリックします。 |
参考
MISRA C:2012: 命令 4.1
ISO/IEC TS 17961: 2013、diverr
CERT C、INT33-C および FLP03-C
CWE、CWE-369
Secure Coding (Embedded Coder)
整数オーバーフローの検出
チェック ID: mathworks.sldv.integeroverflow
モデル内の整数または固定小数点データのオーバーフロー エラーを検出します
説明
このチェックは、整数または固定小数点の演算でのデータ型範囲を超える演算を特定します。
このチェックの推奨事項に従うと、組み込みアプリケーション用の MISRA C:2012 準拠コードと、CERT C 標準、CWE 標準、ISO/IEC TS 17961 標準に準拠するコードが生成される可能性が高くなります。
結果と推奨アクション
結果 | 推奨アクション |
---|---|
失敗。モデルに互換性がない | モデルの非互換性を解決します。次を参照してください。
自動スタブによる非互換性処理も参照してください。 |
モデル内で整数のオーバーフローを検出 | 整数のオーバーフローの原因となる条件を表示するには、ハーネス モデルを作成します。ハーネスのシミュレーションを行うと、入力はエラーを再現します。モデル アドバイザー レポートで [テスト ケースを表示] をクリックします。 |
参考
MISRA C:2012: 命令 4.1
ISO/IEC TS 17961: 2013、intoflow
CERT C、INT30-C および INT32-C
CWE、CWE-190
Secure Coding (Embedded Coder)
非有限で NaN の浮動小数点値の検出
チェック ID: mathworks.sldv.infnan
モデル内の非有限で NaN の浮動小数点値を検出します。
説明
このチェックは、モデル内に出現する非有限で NaN の浮動小数点値を検出します。
結果と推奨アクション
結果 | 推奨アクション |
---|---|
失敗。モデルに互換性がない | モデルの非互換性を解決します。次を参照してください。
自動スタブによる非互換性処理も参照してください。 |
モデル内で、非有限で NaN の浮動小数点値を検出 | 非有限で NaN の浮動小数点値が出現する原因となる条件を確認するには、ハーネス モデルを作成します。ハーネスのシミュレーションを行うと、入力はエラーを再現します。モデル アドバイザー レポートで [テスト ケースを表示] をクリックします。 |
参考
非正規浮動小数点値の検出
チェック ID: mathworks.sldv.subnormal
モデル内の非正規浮動小数点値を検出します。
説明
このチェックは、モデル内に出現する非正規浮動小数点値を検出します。
結果と推奨アクション
結果 | 推奨アクション |
---|---|
失敗。モデルに互換性がない | モデルの非互換性を解決します。次を参照してください。
自動スタブによる非互換性処理も参照してください。 |
モデル内で、非正規浮動小数点値を検出 | 非正規浮動小数点値が出現する原因となる条件を確認するには、ハーネス モデルを作成します。ハーネスのシミュレーションを行うと、入力はエラーを再現します。モデル アドバイザー レポートで [テスト ケースを表示] をクリックします。 |
参考
指定された最小値と最大値の違反の検出
チェック ID: mathworks.sldv.minmax
指定された最小値と最大値を超える信号を検出します
説明
この解析は、モデル全体の中間信号および出力端子について、指定された最小値と最大値 (設計範囲) をチェックします。解析により信号が設計範囲を超えることが検出されると、その結果によりモデルでエラーが発生した場所が特定されます。
このチェックの推奨事項に従うと、組み込みアプリケーション用の MISRA C:2012 準拠コードと、CERT C 標準および CWE 標準に準拠するコードが生成される可能性が高くなります。
結果と推奨アクション
結果 | 推奨アクション |
---|---|
失敗。モデルに互換性がない | モデルの非互換性を解決します。次を参照してください。
自動スタブによる非互換性処理も参照してください。 |
モデル内で最小値/最大値の違反を検出 | 違反の原因となる条件を表示するには、ハーネス モデルを作成します。ハーネスのシミュレーションを行うと、入力はエラーを再現します。モデル アドバイザー レポートで [テスト ケースを表示] をクリックします。 |
参考
MISRA C:2012: 命令 4.1
CERT C、API00-C
CWE、CWE-628
Secure Coding (Embedded Coder)
データ ストアのアクセス違反の検出
チェック ID: mathworks.sldv.dsmaccessviolations
モデルでのデータ ストアのアクセス違反の検出。
説明
このチェックは、以下のデータ ストアのアクセス違反を検出します。
書き込み前の読み取り
読み取り後の書き込み
書き込み後の書き込み
結果と推奨アクション
結果 | 推奨アクション |
---|---|
失敗。モデルに互換性がない | モデルの非互換性を解決します。以下を参照してください。
|
データ ストアのアクセス違反が見つかった | モデル アドバイザー レポートで、[テスト ケースを表示] をクリックします。ハーネス モデルが作成され、そのエラーを再現するテスト ケースが Signal Editor ブロックに表示されます。 |
参考
ブロック入力範囲違反の検出
チェック ID: mathworks.sldv.blockinputrangeviolations
モデルでブロック入力範囲違反を検出します。
説明
このチェックでは、次のような設定をもつブロックの入力範囲違反を検出します。
[範囲外入力の診断] パラメーターが
[警告]
または[エラー]
に設定されているブロックの場合:[default ケースの診断] パラメーターが
[警告]
または[エラー]
に設定されている Multiport Switch ブロック[近似法] パラメーターが
[CORDIC]
に設定されている Trigonometric Function ブロック
メモ
このチェックは、[内挿法] が [Akima スプライン]
または [3 次スプライン]
に設定されている場合、n-D Lookup Table ブロックのブロック入力範囲違反にフラグを立てません。
結果と推奨アクション
結果 | 推奨アクション |
---|---|
失敗。モデルに互換性がない | モデルの非互換性を解決します。以下を参照してください。
|
見つかったブロック入力範囲違反 | モデル アドバイザー レポートで、[テスト ケースを表示] をクリックします。ハーネス モデルが作成され、そのエラーを再現するテスト ケースが Signal Editor ブロックに表示されます。 |
参考
残余演算および逆数演算の使用のチェック
チェック ID: mathworks.sldv.hismviolationshisl_0002
説明
非有限の結果の原因となる rem 演算および reciprocal 演算の使用を特定します。
結果と推奨アクション
条件 | 推奨アクション |
---|---|
モデルまたはサブシステムには、結果として非有限の出力信号を生じる可能性のある、rem 演算または reciprocal 演算が含まれています。非有限の信号は、リアルタイムの組み込みシステムではサポートされていません。 | rem 演算または reciprocal 演算を使用する場合は、対応する入力がゼロにならないよう保護します。 |
参考
Sqrt 演算の使用をチェック
チェック ID: mathworks.sldv.hismviolationshisl_0003
説明
負になる可能性のある入力をもつ Sqrt 演算を特定します。
結果と推奨アクション
条件 | 推奨アクション |
---|---|
モデルの 1 つ以上の Sqrt 演算に、シミュレーション中に負になる可能性のある入力があります。 | Sqrt 演算の入力が負にならないよう保護するために、再モデル化を行います。 |
参考
log 演算および log10 演算の使用をチェック
チェック ID: mathworks.sldv.hismviolationshisl_0004
説明
非有限の結果の原因となる log 演算および log10 演算を特定します。
結果と推奨アクション
条件 | 推奨アクション |
---|---|
モデルで使用される 1 つ以上の log 演算および log10 演算で、非有限数のサポートが必要となる可能性がありますが、これはリアルタイムの組み込みシステムではサポートされていません。 | これらの演算の入力をゼロ以下にならないようにして保護することを検討してください。 |
参考
Reciprocal Sqrt ブロックの使用をチェック
チェック ID: mathworks.sldv.hismviolationshisl_0028
説明
ゼロまたは負になる可能性のある入力をもつ Reciprocal Sqrt ブロックを特定します。
結果と推奨アクション
条件 | 推奨アクション |
---|---|
モデルの 1 つ以上の Reciprocal Sqrt ブロックに、シミュレーション中にゼロまたは負になる可能性のある入力があります。 | Reciprocal Sqrt ブロックの入力が負にならないよう保護するために、再モデル化を行います。 |