使用 Observer Reference 模块进行属性证明分析
此示例向您展示如何使用 Observer Reference 模块执行具有多个属性的属性证明分析，而无需对模型进行更改。在此示例中，您用 Observer Reference 模块替换现有的验证子系统。但是，即使您的模型没有需要替换的验证子系统，您也可以向模型中添加 Observer Reference 模块。有关详细信息，请参阅 使用 Observer 以无线方式访问模型数据 (Simulink Test)。
模型 sldvdemo_debounce_validprop 经过配置用于分析，并试图证明：
在当前输入值和之前的六个输入值为 true 时，输出将为 true。
在当前输入值和之前的六个输入值为 false 时，输出将为 false。
有关 Observer Reference 模块的详细描述，请参阅 使用观察者隔离验证逻辑。
步骤 1：打开模型
sldvdemo_debounce_validprop 模型包含一个名为“验证输出”的验证子系统。有关验证子系统的更多信息，请参阅Verification Subsystem。要打开模型，请输入：
open_system('sldvdemo_debounce_validprop');
步骤 2：用 Observer Reference 模块替换验证子系统
执行以下步骤来创建一个新的 Observer Reference 模块并替换验证输出验证子系统。
1.右键点击验证输出子系统。在上下文菜单中，点击观察者 > 将选定的模块移动到 Observer > 新建 Observer。
2.在出现的对话框中点击是。
3.Observer Reference 模块取代了验证子系统。sldvdemo_debounce_validprop_Observer1Observer 模型打开。
4.将 sldvdemo_debounce_validprop_Observer1 保存在 MATLAB 路径下的可写文件夹中。
5.双击其中一个 Observer Port 模块以打开“管理 Observer 模块”窗口。这两个信号，debounce 和 raw，会自动映射到 sldvdemo_debounce_validprop_Observer1 Observer 模型中的两个 Observer Port 模块。
步骤 3：执行属性证明分析
要进行属性证明分析，请按照以下步骤操作：
1.在顶层模型中的 Design Verifier 选项卡上，点击证明属性。
2.分析完成后，Simulink Design Verifier 结果摘要窗口报告两个目标已满足。
3.打开 HTML 分析报告即可查看包含有关顶层模型和观察者的信息的详细报告。
步骤 4：审查属性证明分析报告
分析报告在“属性”章节的“观察器模型”部分显示了用于属性验证的观察器信息。
步骤 5：清理
关闭模型。
bdclose('sldvdemo_debounce_validprop');
