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

この例について

以下の節では、Proof Objective ブロックを使用して指定するプロパティを証明する Simulink^® モデルについて説明します。この例では、Simulink Design Verifier™ のプロパティ証明機能について解説します。

この例では、以下のタスクを実行します。

タスク	説明	参照先
1	モデル例を作成します。	モデル例の作成
2	モデルが Simulink Design Verifier と互換であることを検証します。	モデル例の互換性のチェック
3	Proof Objective ブロックをモデルに追加して、その証明の準備を行います。	モデル例のインストルメント化
4	Simulink Design Verifier をプロパティ証明用に構成します。	プロパティ証明オプションの構成
5	モデルのプロパティを証明します。	モデル例の解析
6	解析結果をレビューします。	解析結果のレビュー
7	証明前提を追加して解析の制約を指定します。	例の証明のカスタマイズ
8	カスタマイズされたモデルのプロパティを証明してその結果を解釈します。	モデル例の再解析

モデル例の作成

この例で使用する Simulink モデルを作成します。

空の Simulink モデルを作成します。
次のブロックを空のモデルウィンドウにコピーします。
- Sources ライブラリの Inport ブロック。これにより Simulink Design Verifier が値を制御する入力信号を初期化
- Logic および Bit Operations ライブラリから、単純なロジックを提供する Compare To Zero ブロック
- Sinks ライブラリから、出力信号を受け取る Outport ブロック
モデルが次のようになるように、これらのブロックを接続します。
[モデル化] タブで、[モデル設定] をクリックします。
[コンフィギュレーションパラメーター] ダイアログボックスの [ソルバー] ペインの [ソルバーの選択] で、次を行います。
- [タイプ] オプションを [固定ステップ] に設定します。
- [ソルバー] オプションを [離散 (連続状態なし)] に設定します。
Simulink Design Verifier は、固定ステップソルバーを使用するモデルのみ解析できます。
[OK] をクリックして変更を保存し、[コンフィギュレーションパラメーター] ダイアログボックスを閉じます。
モデルを ex_property_proving_example_basic という名前で保存します。

モデル例の互換性のチェック

Simulink Design Verifier ソフトウェアがモデルを解析する際、解析の開始前に必ず互換性チェックが実行されます。モデルに互換性がない場合、解析できません。

解析を開始する前に、モデルが Simulink Design Verifier と互換であるかどうかも確認できます。

ex_property_proving_example_basic モデルを開きます。
[Design Verifier] タブで、[互換性チェック] をクリックします。
Simulink Design Verifier ソフトウェアが、モデルに互換性があるかどうかを示すログウィンドウを表示します。
ここで作成したモデルは互換性があります。

モデルが部分的に互換である場合

互換性チェックによりモデルが部分的に互換であることが示された場合、モデルには Simulink Design Verifier でサポートされないオブジェクトが少なくとも 1 つ含まれています。部分的に互換なモデルは解析可能ですが、既定では、サポートされないオブジェクトはスタブされます。解析結果は不完全になる場合があります。自動スタブの詳細は、自動スタブによる非互換性処理を参照してください。

モデル例のインストルメント化

モデルのプロパティを Simulink Design Verifier で証明できるように、モデル例を準備します。具体的には、Proof Objective ブロックを追加して構成し、モデルをインストルメント化します。

MATLAB^® コマンドウィンドウに sldvlib と入力します。
Simulink Design Verifier ライブラリが表示されます。
Objectives and Constraints サブライブラリを開きます。
Proof Objective ブロックをモデルにコピーして、それを Compare To Zero ブロックと Outport ブロックの間に挿入します。
モデルの Proof Objective ブロックをダブルクリックします。
Proof Objective ブロックのパラメーターダイアログボックスが開きます。
[値] ボックスに「1」と入力します。
Simulink Design Verifier ソフトウェアは、Compare To Zero ブロックで出力された信号が受け取った任意の信号に対してこの値に常に到達することを証明しようとします。
[OK] をクリックして変更を適用し、Proof Objective ブロックパラメーターのダイアログボックスを閉じます。
モデルを保存して、それを開いたままにします。

プロパティ証明オプションの構成

インストルメント化した ex_property_proving_example_basic モデルのプロパティ証明を行うよう、Simulink Design Verifier を構成します。

ex_property_proving_example_basic モデルを開きます。
[Design Verifier] タブの [モード] セクションで、[プロパティ証明] を選択します。
[プロパティ検証設定] をクリックします。
[OK] をクリックして、変更を適用して [コンフィギュレーションパラメーター] ダイアログボックスを閉じます。
メモ
必要に応じて、[プロパティ証明] ペインで、Simulink Design Verifier によるモデルのプロパティ証明を制御する他のパラメーターの値を指定することができます。詳細は、Design Verifier ペイン: プロパティ証明を参照してください。
ex_property_proving_example_basic モデルを保存します。

モデル例の解析

ex_property_proving_example_basic モデルを解析するには、[Design Verifier] タブで [プロパティの証明] をクリックします。Simulink Design Verifier がプロパティ証明解析を開始します。

解析中、ログウィンドウには解析の進行状況が表示されます。ここには、処理されたオブジェクティブ数や達成された、あるいは反証されたオブジェクティブについての情報が表示されます。

解析を任意の時点で終了するには、ログウィンドウで [停止] をクリックします。

解析結果のレビュー

解析が完了すると、ログウィンドウには結果をレビューするために次のようなオプションが表示されます。

モデルの解析結果の強調表示
詳細な HTML 解析レポートの生成
テストケースを含むハーネスモデルの作成
モデルで作成されたテストケースのシミュレートおよびモデルカバレッジレポートの生成

Simulink Design Verifier データファイルを表示することもできます。このデータファイルの詳細は、Simulink Design Verifier データファイルの管理を参照してください。

以下の節では、解析結果をレビューする方法を説明します。

モデルの結果のレビュー
詳細な解析レポートのレビュー
ハーネスモデルのレビュー
反例によるモデルのシミュレーション
解析結果のレビュー

モデルの結果のレビュー

モデルウィンドウでブロックを強調表示させることで、解析結果を一目でレビューできます。強調表示には次の 4 色があります。

グリーン — すべての証明オブジェクティブが有効と証明された。
レッド — 証明オブジェクティブが反証され、そのオブジェクティブを反証する反例が生成された。
オレンジ — 証明オブジェクティブは反証されたが、反例が生成できなかったか、証明オブジェクティブが依然として判定されていない。これは次により発生します。
- Constant ブロックなど、このソフトウェアが制御できない値をもつ信号についての証明オブジェクティブ
- 非線形計算に依存する証明オブジェクティブ
- ゼロ除算など、算術エラーを生成する証明オブジェクティブ
- 自動スタブの有効化時に、解析で反例の生成に必要だがその操作が認識されない、未サポートのブロックが検出された
- 解析のタイムアウト
- 解析エンジンの制限
グレー — モデルオブジェクトが解析に含まれていなかった。

モデル例の解析結果を強調表示します。

ex_property_proving_example_basic 解析の [結果の概要] ウィンドウで、[解析結果をモデル上で強調表示] をクリックします。
Proof Objective ブロックはレッドで強調表示されます。これは証明オブジェクティブが反例によって反証されたことを示します。
Simulink Design Verifier の [結果] ウィンドウが表示されます。
モデルのオブジェクトをクリックすると、ウィンドウが変化してそのオブジェクトの詳細な解析結果が表示されます。
ヒント
既定では、Simulink Design Verifier の [結果] ウィンドウは常に最前面に表示されます。ウィンドウが他のウィンドウの背面に移動できるようにするには、をクリックして [常に手前に表示] をオフにします。
強調表示された Proof Objective ブロックをクリックします。
Simulink Design Verifier の [結果] ウィンドウには、Compare to Zero からの出力信号が 1 でない証明オブジェクティブが反例によって反証されたことが示されます。

詳細な解析レポートのレビュー

詳細な HTML 解析レポートは次により作成します。

Simulink Design Verifier の [結果の概要] ウィンドウで、[詳細な解析レポートを生成] をクリックします。
HTML レポートがブラウザーウィンドウで開きます。
レポートには次の目次が含まれます。ハイパーリンクをクリックしてレポートの個別の節に移動します。
目次で Summary をクリックします。
概要には解析結果がまとめられており、Simulink Design Verifier がモデルにおいて 1 つのオブジェクティブが反証された反例を確認したことが示されています。
目次で Proof Objectives Status をクリックします。
[反例によって反証されたオブジェクティブ] の表は、Simulink Design Verifier が生成した反例を使用して反証された証明オブジェクティブの一覧です。モデルウィンドウ内でオブジェクティブを特定するには、Proof Objective をクリックします。モデルウィンドウの対応する Proof Objective ブロックが強調表示されます。
[反例によって反証されたオブジェクティブ] の表の [反例] 列の 1 をクリックします。
この節には、証明オブジェクティブ 1 に関する情報が表示され、Simulink Design Verifier がそのオブジェクティブを反証するために生成した反例の詳細が示されます。この反例では、信号値 99 が、Proof Objective ブロックにより指定されたオブジェクティブが反証しています。つまり、99 は 0 以下でないため、Compare To Zero ブロックは 1 (true) でなく 0 (false) を返すことになります。

ハーネスモデルのレビュー

モデルの証明オブジェクティブを反証する反例を含むハーネスモデルを作成します。

Simulink Design Verifier のログウィンドウで、[ハーネスモデルの作成] をクリックします。
ex_property_proving_example_basic_harness という名前のハーネスモデルが作成されます。
このハーネスモデルには次の項目が含まれています。
- Inputs という名前の Signal Builder ブロック — 証明オブジェクティブを反証する信号のグループ。
- Test Unit という名前の Subsystem ブロック — モデルのコピー。
- Test Case Explanation という名前の DocBlock — 解析により生成される反例についてのテキストによる説明。
- Size-Type ブロック — 信号を Inputs ブロックから Test Unit ブロックに送信するサブシステム。このブロックは、信号のサイズおよびデータ型が Test Unit ブロックと一致することを検証します。
Inputs ブロックをダブルクリックします。
入力信号 1 により、Compare to Zero ブロックの出力は 0 になります。この反例は、Compare to Zero ブロックの出力を 1に指定している証明オブジェクティブに違反します。

反例によるモデルのシミュレーション

ハーネスモデルのシミュレーションを実行して、モデルの証明オブジェクティブが反証される反例を観測します。

ex_property_proving_example_basic モデルを開きます。
[シミュレーション] タブで [ライブラリブラウザー] をクリックします。
Sinks ライブラリから Scope ブロックをハーネスモデルウィンドウにコピーします。Scope ブロックにより、モデルの Compare To Zero ブロックで出力された信号の値が表示できます。
ハーネスモデルウィンドウで、Test Unit サブシステムの出力信号を Scope ブロックに接続します。
ハーネスモデルをシミュレートするには、[シミュレーション] タブで [実行] をクリックします。
Simulink ソフトウェアがハーネスモデルのシミュレーションを実行します。
ハーネスモデルウィンドウで、Scope ブロックをダブルクリックして表示ウィンドウを開きます。
Scope ブロックにモデルの Compare To Zero ブロックで出力された信号の値が表示されます。この例では、Compare To Zero ブロックはシミュレーション全体を通じて 0 (false) を返し、これにより Compare to Zero ブロックの出力が 1 (true) であるという証明オブジェクティブが反証されます。Signal Builder ブロックが提供した反例により、証明オブジェクティブが反証されます。

解析結果のレビュー

モデルが開いたままであれば、[結果の概要] ウィンドウで最新の Simulink Design Verifier の解析結果を表示できます。

[Design Verifier] タブの [結果の確認] セクションで、[結果の概要] をクリックします。[結果の概要] ウィンドウが開き、最新の Simulink Design Verifier の解析結果が表示されます。

[結果の概要] ウィンドウからは、任意の Simulink Design Verifier 解析に対して次のタスクを実行できます。

タスク	参照先
モデルにおける、解析結果の強調表示。	モデルにおける結果の強調表示
詳細な解析レポートの生成。	結果の確認
ハーネスモデルの作成。または既に存在する場合はモデルの開始。解析時に反例が作成されなかった場合、このオプションは使用できません。	Simulink Design Verifier ハーネスモデルの管理
データファイルの表示。	Simulink Design Verifier データファイルの管理
ログファイルの表示。	ログファイルの表示

モデルを閉じると、解析結果は表示できなくなります。

例の証明のカスタマイズ

前のタスクで Simulink Design Verifier が反証した証明オブジェクティブをもつ単純な Simulink モデルを変更します。具体的には、Proof Assumption ブロックの追加と構成により証明をカスタマイズします。

MATLAB コマンドウィンドウで「sldvlib」と入力します。
Simulink Design Verifier ライブラリが開きます。
Objectives and Constraints サブライブラリを開きます。
Proof Assumption ブロックをモデルにコピーします。
モデルウィンドウで、Proof Assumption ブロックを Inport ブロックと Compare To Zero ブロックの間に挿入します。
モデル内で、Proof Assumption ブロックをダブルクリックしてその属性にアクセスします。
Proof Assumption ブロックのパラメーターダイアログボックスが開きます。
[値] ボックスに「[-1, 0]」と入力します。このモデルのプロパティを証明する際、Simulink Design Verifier は、Compare To Zero ブロックに入る信号値をこの指定された範囲に制約します。Compare to Zero ブロックへの入力が常にこの範囲内であれば、Compare to Zero ブロックの出力は常に 1 になります。
[適用]、[OK] をクリックして、変更を適用し、Proof Assumption ブロックパラメーターのダイアログボックスを閉じます。
ex_property_proving_example_basic モデルを保存して、それを開いたままにします。

モデル例の再解析

変更したモデルを解析して、Proof Assumption ブロックがプロパティ証明解析にどう影響するかを確認します。

ex_property_proving_example_basic モデルを開きます。[Design Verifier] タブで、[プロパティの証明] をクリックします。

解析が完了すると、ログウィンドウにオプションが表示されます。解析でモデルのすべての証明オブジェクティブが達成され、反例がないため、ハーネスモデルを作成するオプションはありません。

2 番目の解析結果のレビュー

2 番目の解析結果をレビューします。

モデルの結果のレビュー
解析レポートのレビュー

モデルの結果のレビュー

モデルを強調表示して、解析結果を確認します。

[解析結果をモデル上で強調表示] をクリックします。
ここで、Proof Objective はグリーンに強調表示されます。
Proof Objective ブロックをクリックします。
Simulink Design Verifier の [結果] ウィンドウには、信号が 1 であることを示す証明オブジェクティブが有効であることが示されます。

解析レポートのレビュー

詳細レポートで解析結果をレビューします。

[詳細な解析レポートを生成] をクリックします。
目次で Summary をクリックします。
概要の章には、Simulink Design Verifier がモデル内の証明オブジェクティブを証明したことが示されます。
制約の節には、Proof Assumption ブロックで指定された解析の制約がリストされています。
スクロールしてブラウザーウィンドウの一番上まで戻ります。目次で Proof Objectives Status をクリックします。
有効と証明されたオブジェクティブの表には、Simulink Design Verifier が有効性を証明した証明オブジェクティブがリストされます。
Properties の章が表示されるまで下にスクロールするか、ブラウザーウィンドウの一番上に移動し、目次で Properties をクリックします。
証明オブジェクティブの概要には、モデル内で指定したオブジェクティブを Simulink Design Verifier が証明したことが示されます。Proof Assumption ブロックでは、入力信号の領域を [-1, 0] の区間に制限します。そのため、このソフトウェアはこの区間にゼロより大きい値は含まれないことを証明し、証明オブジェクティブを達成させます。

矛盾モデルの解析

解析によりエラー「The model is contradictory in its current configuration」が生成される場合、モデル内に矛盾が検出されているため、モデルを解析できません。無効なパラメーターをもつ Proof Assumption ブロックがモデルにある場合、矛盾が生じることがあります。たとえば、信号が定数 10 であるときに前提で信号は 0 ～ 5 でなければならないと記述している場合などです。

矛盾が検出されると、前のすべての結果は無効にされ、すべてのプロパティが反証されたことがレポートされます。

メモ

設計の最小値/最大値またはテスト条件/証明の前提を介して入力時に追加される制約により、矛盾が生じることはありません。ただし、テスト条件/証明の前提を使用する計算の下流である信号を制約する場合は、制約される条件がモデル計算を通じて実行可能であることを確認しなければなりません。そうしないと、結果として得られるモデルに矛盾が生じ、明示的な解析エラーの有無にかかわらず結果が無効となる可能性があります。制約が実行可能であることを確認するには、最初にテストオブジェクティブを使用して同じ条件を試します。それが達成可能であれば、同じ条件を制約として安全に使用できます。

大規模モデルでのプロパティの証明

モデルの完全な証明を行うには、モデルが到達可能なコンフィギュレーションが、長時間の遅延後に到達するものも含め、すべて Simulink Design Verifier によって検索される必要があります。モデルの完全な検索に必要な計算時間およびメモリによっては、包括的な証明は実際的ではありません。

大規模モデルのプロパティの証明では、大規模モデルのプロパティ証明解析のパフォーマンスの向上に利用可能な方法についての詳細が記載されています。