颞运营商

的万博1manbetxSimulink®Design Verifier™库提供了三个基本的时态操作符块，可用于建模时态属性。时态操作符的目的是支持时态需求的规范，这样建模的属性与实际的文本需求有更紧密的关联。万博1manbetx这些块是用于构造更复杂的时态属性的低级构建块。

电动车窗控制器

电动车窗控制器通过发出将车窗上下移动的指令来响应驾驶员和乘客的命令。它也响应障碍和达到窗框的末端在任何方向。

考虑一下电源窗口控制器的以下两个要求:

要求1(障碍反应)

当检测到障碍物时，控制器发出向下指令，持续1秒。

需求2(自动停机特性)

如果驾驶员按下按钮少于1秒，控制器就会持续发出down命令，直到到达结束或驾驶员按下向上按钮。

%电源窗口控制器的模型open_system (“sldvdemo_powerwindowController”) open_system (“sldvdemo_powerwindowController /控制”)

属性规范

power window验证系统是顶级模型，它包含了一个对power window控制器模型的模型引用，该模型指定了控制器行为和建模需求。

%顶层验证系统的模型open_system (“sldvdemo_powerwindow_vs”)

全球的假设:电源窗口控制器是一个开放的系统。这使得环境控制输入、障碍和终止(窗口框的末端)可以自由地发生。要约束环境，为控制器模型添加两个全局假设。

1)障碍和终点输入永远不会同时实现。

2)在接下来的1秒间隔内，障碍不会出现多次。

对于障碍物的时间假设，使用输出类型为“延时固定持续时间”的检测器块捕获1秒的固定持续时间(5个时间步，0.2个采样时间)。

%全球假设open_system (“sldvdemo_powerwindow_vs /全球假设”)

现在考虑第一个控制器需求障碍的反应。

%障碍响应open_system (“sldvdemo_powerwindow_vs /验证Subsystem2”)

在这里，对于属性规范使用输出类型为“Delayed Fixed Duration”的检测器块。检测到障碍物后，构建4步的固定间隔。注意，对于输出类型为“延时固定持续时间”的检测器，在输出构建阶段不会观察到输入。如果在没有假设的情况下，障碍可以自由出现，那么您可能希望观察所有中间出现的障碍。这可以通过4个时间步骤的“有限”扩展时间块来实现。

现在考虑AutoDown特性的电源窗口控制器。

为便于说明，请将此属性规范分成较小的部分:

一旦您有了这个初始属性规范，您就可以使用它来通过Simulink Design Verifier进行属性验证。万博1manbetx你会得到这个属性的一个反例。反例显示了一个场景，在该场景中，当控制器由于对先前检测到的障碍的响应而处于紧急停机状态时，给出了down命令。在您添加了一个约束以避免这种情况发生后，您将得到另一个反例:如果在先前给出up命令时按下了down按钮，那么自动向下功能将被禁用，只有按下了down按钮时，才会给出down命令。查看这些反例并观察模型，您可以看到这样一种模式，即只有当控制器处于中立状态时，即驾驶员按下按钮时，AutoDown特性才会启用。

通过强制控制器输出为中立的——up和down命令都不为真——作为AutoDown属性的先决条件来合并这个约束。此属性被证明有效。

%有效AutoDownopen_system (“sldvdemo_powerwindow_vs /验证Subsystem3”)

为属性验证生成测试用例

一旦指定了属性，除了属性证明之外，您还可以运行Simulink Design Verifier来自动生成测试用例，以执行属性中的各种条件。万博1manbetx这可以通过将自定义测试目标块放置在属性的适当位置来实现。

放置测试目标块(具有“true”值)的一个这样的位置是在输入到隐含块的第一个输入的信号上(如上面的属性所示)。在运行测试生成时，该测试目标得到满足，您将得到一个测试用例，该测试用例执行属性中编码的各种约束。万博1manbetxSimulink Design Verifier也可以创建一个测试工具来模拟这个测试用例。带有相关信号的信号生成器模块如下所示。

现在可以模拟这个测试用例，并通过放置一个范围来显示两个检测器块和No_Cmd的输入和输出值，来查看如何在属性中创建时间持续时间。

手动检查测试用例值可以让您看到指定的属性是否按预期的方式运行。

这个测试目标块有助于识别一个场景，在这个场景中属性是有效的，而暗指块不是简单的true。当一个暗指块的输出为真，因为它的第一个输入是假的时候，它通常为真。当您得到一个满足这个测试目标的测试用例时，您知道至少有一种情况，隐含块的第一个输入为真。

这个练习可以通过手动检查由Simulink Design Verifier自动生成的测试用例来帮助您验证您的属性规范。万博1manbetx

清理

要完成示例，请关闭所有打开的模型。

close_system (“sldvdemo_TOBlocks”, 0);close_system (“sldvdemo_powerwindowController”, 0);close_system (“sldvdemo_powerwindow_vs”, 0);