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

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

open_system('sldvdemo_sbr_verification');