Main Content

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

MATLAB Function ブロックを使用したプロパティ証明

この例では、シート ベルト リマインダーの設計モデルを検証する方法を示します。その下の Safety Properties ブロックには、アイコンをアクティブにすべきタイミングを示す MATLAB で指定されたプロパティが含まれます。Simulink Design Verifier は正確性を証明または反例を同定するために、設計モデルおよび安全性プロパティを解析します。このモデルでは、設計でキー入力が 0 で開始されて 1 のインクリメントで変更されると仮定されるため、プロパティ違反が発生します。

open_system('sldvdemo_sbr_verification');