使用 Observer Reference 模块进行属性证明分析

此示例使用:

此示例向您展示如何使用 Observer Reference模块执行具有多个属性的属性证明分析，而无需对模型进行更改。在此示例中，您用 Observer Reference模块替换现有的验证子系统。但是，即使您的模型没有需要替换的验证子系统，您也可以向模型中添加 Observer Reference模块。有关更多信息，请参阅使用观测器以无线方式访问模型数据 (Simulink Test) 。

模型sldvdemo_debounce_validprop 经过配置用于分析，并试图证明：

当当前输入值和之前的六个输入值为真时，输出将为真。
当当前和之前的六个输入值为假时，输出也将为假。

有关 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：审查财产证明分析报告

分析报告显示了“属性”一章的“Observer模型”部分中用于证明属性的Observer信息。

步骤5：清理

关闭模型。

bdclose('sldvdemo_debounce_validprop');