モデルの解析と結果の解釈
Simulink® Design Verifier™ の解析ワークフローにより検証プロセスが効率化され、モデルの準備から結果の解釈まで順番に実行できます。Simulink Design Verifier を使用すると、モデルの信頼性を向上させて開発時間を短縮でき、システム設計の信頼度を高めることができます。
Simulink Design Verifier ワークフローでは、Simulink モデルまたは要件を入力として解析用に準備します。
次に、Simulink Design Verifier で以下を行う解析モードを使用して、Simulink モデルを解析します。
モデル カバレッジを達成するテスト ケースの生成。
実行時に発生する可能性のある設計エラーの検出。
プロパティ証明およびプロパティ違反の特定。
解析が完了したら、結果を確認して設計エラーを特定するか、モデル プロパティを検証します。ワークフローの最後に、解析結果をレビューするか、結果をエクスポートしてテスト ハーネスを作成します。
このチュートリアルのワークフローでは、Simulink Design Verifier の解析手順を重点的に扱います。
モデルの互換性チェック
Simulink Design Verifier では、モデルを解析する前に、モデルが解析に対して互換性があるかどうかをチェックします。モデルの互換性の詳細については、解析のためのモデルの互換性チェックを参照してください。ソフトウェアではモデルの互換性チェックが実行され、モデル表現が作成されます。モデル表現には、解析時に使用できるモデル アーティファクトが含まれています。互換性チェックにより、モデルに完全な互換性があるのか、部分的な互換性があるのか、互換性がないのかがわかります。
Simulink ではモデルのソフトウェアの機能を広くサポートしますが、Simulink Design Verifier ではサポートされない機能も一部あります。詳細については、解析でサポートされていない Simulink ブロックおよびSimulink ソフトウェア機能に対する Simulink Design Verifier の制限事項を参照してください。
ブロック置換ルールの適用
解析用に、モデルの互換性の制限を回避する場合またはモデル要素をカスタマイズする場合は、Simulink Design Verifier のブロック置換ルールを使用。詳細については、ブロック置換を使用した解析の実行を参照してください。
解析時にモデルのパラメーターに対し値を追加生成する場合は、Simulink Design Verifier のパラメーター コンフィギュレーションを使用。詳細については、Use Parameter Configuration in Analysisを参照してください。
Simulink Design Verifier オプションの設定
[コンフィギュレーション パラメーター] ダイアログ ボックスで Simulink Design Verifier の解析オプションを設定できます。あるいは、関数 sldvoptions を使用して、コマンド ラインで Simulink Design Verifier オプションを指定することもできます。詳細については、モデルの解析オプションの構成を参照してください。
モデルの解析の実行
以下についてモデルを解析できます。
設計エラー検出: 実行時に発生する可能性のある設計エラーの検出。詳細については、モデルにおける設計エラーの解析を参照してください。
テスト ケースの生成: モデル カバレッジを達成するテスト ケースの生成。詳細については、Workflow for Test Generationを参照してください。
プロパティ証明解析: プロパティ証明およびプロパティ違反の特定。詳細については、モデル プロパティ証明のワークフローを参照してください。
モデルでテスト ケースの生成またはプロパティの証明を行う場合は、整数オーバーフローおよびゼロ除算について設計エラー検出を実行。詳細については、以下のトピックを参照してください。
解析結果の生成
Simulink Design Verifier でモデルの解析が完了すると、解析のハイライトおよび結果オプションが [結果の概要] ウィンドウに表示されます。詳細については、モデルの解析の実行を参照してください。
解析結果の解釈
解析結果を確認し、HTML、DOCX、または PDF 形式で解析レポートを生成できます。詳細については、解析結果のレビューを参照してください。
Simulink Design Verifier では、モデルの解析ごとにログ ファイルが作成されます。
ログ ファイルを表示するには、Simulink Design Verifier のログ ウィンドウで [ログの表示] をクリックします。
ログ ファイルは .txt 形式で生成されます。現在のロケールのものでない文字はログ ファイルで文字化けします。
ログ ファイルには、モデルの各オブジェクトの解析結果のリストが含まれます。ログ ファイルの内容は、解析時にログ ウィンドウに表示される解析結果に対応します。
Simulink Design Verifier ブロック ライブラリ
Simulink Design Verifier ブロック ライブラリには、3 つのブロックのカテゴリがあります。
Objectives and Constraints — カスタムのオブジェクティブおよび制約を定義するブロック
Temporal Operators — Boolean 信号で時相プロパティを定義するブロック
Verification Utilities — 各種検証ユーティリティ
Simulink Design Verifier ブロック ライブラリを開くには、MATLAB® コマンド プロンプトで sldvlib と入力します。
ブロック ライブラリには、モデルの一般的なプロパティの指定例を含む Example Properties サブライブラリもあります。これらの例は、自分のモデルに合わせて簡単に変更できます。
参考
モデルにおける設計エラーの解析 | ブロック置換を使用した解析の実行
