Main Content

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

プロパティ証明では、設計エラー検出およびテスト生成と同様の基本手法が使用され、同じパフォーマンス制限が課されます。ただし、設計エラー検出やテスト生成とは異なり、多くの場合、結果の有効性を保ったまま問題を単純化することができません。

モデル ダイナミクスによる影響を受けない単純な証明オブジェクティブは迅速に証明できます。しかし、完全な証明を行うには、モデルが到達可能なコンフィギュレーションが、長時間の遅延後に到達するものも含め、すべて Simulink® Design Verifier™ によって検索される必要があります。モデルの完全な検索に必要な計算時間およびメモリによっては、包括的な証明は実際的ではありません。

大規模モデルでプロパティ証明のパフォーマンスの向上に使用できる手法は 2 つあります。

モデルの設計時にプロパティ違反を見つける

Simulink Design Verifier ソフトウェアには、大規模で複雑なモデルにおいて迅速にプロパティ違反を特定する手法が用意されています。モデルの設計時にこの手法を使用してモデルを解析することで、設計を完了する前にプロパティ違反を修正できます。

モデルのプロパティ違反を特定するには、[コンフィギュレーション パラメーター] ダイアログ ボックスの [Design Verifier]、[プロパティ証明] ペインで、[手法] パラメーターの値を [FindViolation] に指定します。この手法を使用すると、[最大違反ステップ数] パラメーターがアクティブになり、検索でタイム ステップ数の上限を指定できます。

モデルの解析時に、指定されたタイム ステップ数内のプロパティ違反のみを検索します。最初にプロパティ違反を特定し、それを修正して、Prove の手法を使用するプロパティ証明解析のパフォーマンスを向上させます。

違反が検出されない場合、指定された制限より少数のタイム ステップをもつ入力シーケンスでプロパティに違反することは不可能になります。ただし、指定された制限より多いタイム ステップ内に反例があるかもしれないので、プロパティが true であることを証明することはできません。

プロパティの証明と証明違反の検出の組み合わせ

大規模モデルでプロパティを証明するために次の手法を使用します。この手法は証明と違反の検索を組み合わせたものです。

  1. [Design Verifier]、[プロパティ証明] ペインで、[手法] パラメーターを [Prove] に設定します。

  2. [Design Verifier] ペインの [最大解析時間] パラメーターには、5 ～ 10 分など、比較的短い値を使用します。自明な反例が存在する場合またはプロパティがモデル ダイナミクスに依存しない場合、解析はその時間内で完了するはずです。

  3. [手法] パラメーターを [FindViolation] に変更して、[最大違反ステップ数] パラメーターに、4、5、6 などの小さな限界を選択します。プロパティに単純な反例がある場合、このソフトウェアはそれを検出します。

  4. 小さな範囲で違反が見つからない場合、範囲を広げて長い反例を検索します。

    1. 範囲を数段階大きくして、時間とメモリの消費の処理を観察します。システム リソースにより検索可能な違反の長さが制限されることがあります。

    2. また、モデルのダイナミクスと任意のコンフィギュレーションのペア間の遷移に必要なタイム ステップ数について検討します。選択した範囲が大き過ぎると、違反の検索は制限のない証明より複雑になることがあります。

  5. 比較的大きな範囲で違反の検索を実行できる場合 (たとえば、30 ～ 50 タイム ステップなど)、[Prove] 手法に切り替えて、数時間など、より長い時間制限を使用します。