Main Content

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

要件のモデル化

プロパティ証明を使用した設計要件のモデル化および検証

ブロック

Proof Assumptionモデルのプロパティを証明する場合に、信号値を制限する
Proof Objectiveモデルのプロパティを証明する場合に信号で達成されなければならないオブジェクティブを定義する
Assertion信号がゼロかどうかのチェック
Detector入力が true となる期間の検出と、出力タイプに基づく出力が true となる期間の作成
Extender入力が true となる期間の延長
Implies特定の応答を生成する条件の指定
Within Implies目的の期間内に応答が発生するかを確認する
Verification Subsystemシミュレーション結果や生成済みのコードに影響を与えることなく、証明オブジェクティブまたはテスト オブジェクティブを指定する

関数

sldv.assumeStateflow チャートおよび MATLAB Function ブロックについて証明の前提となる関数
sldv.proveStateflow チャートおよび MATLAB Function ブロックの証明オブジェクティブ関数
sldvextractサブシステムまたはサブチャートの内容を解析用の新しいモデルに抽出する
sldvoptions設計検証オプション オブジェクトの作成
sldvrunモデルの解析
sldvreportSimulink Design Verifier レポートを作成する

トピック

プロパティ証明とは

プロパティ証明の概要。

モデル プロパティ証明のワークフロー

モデルのプロパティを証明する処理の概要を説明します。

モデルのプロパティの証明

モデル プロパティを証明する過程を、例を使って順に確認していきます。

検証モデルを使用したシステムレベル プロパティの証明

検証モデルを使用してシステムレベル プロパティを証明する例。

サブシステムのプロパティの証明

サブシステムのプロパティを証明する方法を説明します。

モデル スライサーを使用したプロパティ証明違反のデバッグ

モデル スライサーを使用したプロパティ証明違反のデバッグ

モデルのプロパティの設計と検証

Simulink® Design Verifier™ を使用して、設計要件をプロパティとしてモデル化し、モデル内のプロパティを証明することができます。

パラメーター制約値

Simulink® Design Verifier™ による解析のパラメーター コンフィギュレーションの概要。

モデル要件

Simulink Design Verifier ブロック ライブラリにはサブライブラリ Example Properties が含まれています。

パラメーターの制約値の定義

解析でパラメーターを変数として指定する方法の例。

フル カバレッジのためのパラメーター制約値の指定

パラメーター制約値の指定によりフル モデル カバレッジを達成する方法の例。

Design Verifier ペイン: プロパティ証明

Simulink Design Verifier による解析モデルのプロパティ証明方法を制御するオプションを指定します。

Design Verifier ペイン: パラメーター

Simulink Design Verifier によるモデル解析時のパラメーター コンフィギュレーションの使用を制御するオプションを指定します。

解析結果のレビュー

Simulink Design Verifier の [検証結果の概要] ウィンドウで解析結果をレビューする。

仕様モデルとは

仕様モデルおよび要件に基づく検証での使用に関する概要。

注目の例