电源窗口控制器时间属性
这个例子展示了如何在一个电源窗口控制器模型中建模时间系统需求，使用Simulink®Design Verifier™temporal Operator模块进行性能证明和测试用例生成。金宝app
颞运营商
的金宝appSimulink®Design Verifier™库提供三个基本的时态运算符块，可用于建模时态属性。临时操作符的目的是支持临时需求的规范，这样建模的属性与实际的文本需求有更紧密的关联。金宝app这些块是用于构造更复杂的时态属性的低级构建块。
电动车窗控制器
电动车窗控制器响应司机和乘客的命令，发出将车窗向上或向下移动的命令。它还能对障碍物作出反应，并在任何方向上到达窗框的末端。
电动窗控制器需要考虑以下两点要求:
要求1(障碍反应)
当检测到障碍物时，控制器发出down命令1秒。
需求2(自动下线特性)
如果驾驶员按下向下按钮的时间小于1秒，则控制器会一直发出向下命令，直到到达终点或驾驶员按下向上按钮。
%电动窗控制器型号open_system (“sldvdemo_powerwindowController”) open_system (“sldvdemo_powerwindowController /控制”）
属性规范
功率窗口验证系统是顶级模型，它包含一个对功率窗口控制器模型的模型引用，该模型指定了控制器行为和建模的需求。
%顶级验证系统模型open_system (“sldvdemo_powerwindow_vs”）
全球的假设:电动窗控制器是一个开放系统。这使得环境控制的输入、障碍和终止点(窗口框架的末端)可以自由地发生。为了约束环境，为控制器模型添加两个全局假设。
1)障碍和终点输入永远不会同时成真。
2)在接下来的1秒间隔内没有出现多次障碍。
对于障碍物的时间假设，使用输出类型为“Delayed Fixed Duration”的检测器块捕捉1秒的固定时间(5个时间步长，样本时间为0.2)。
%全球假设open_system (“sldvdemo_powerwindow_vs /全球假设”）
现在考虑第一个控制器要求障碍的反应．
%障碍响应open_system (“sldvdemo_powerwindow_vs /验证Subsystem2”）
在这里，属性规范使用输出类型为“Delayed Fixed Duration”的Detector块。检测到障碍物后，构建4步的固定间隔。注意，对于“Delayed Fixed Duration”输出类型的检测器，在输出构造阶段不会观察到输入。如果障碍可以在没有假设的情况下自由出现，您可能希望观察所有中间出现的障碍。这可以通过Extender块与“有限的”延长时间4个时间步骤实现。
现在考虑AutoDown特性电源窗口控制器的。
为了举例说明，考虑这个属性说明的小部分:
感兴趣的第一个时间持续时间，“司机按下按钮小于1秒”，被Detector1捕获。采样率为0.2时，将1秒间隔分解为5个时间步。在检测下行信号时，Detector1在其输出处构造一个5步固定的时间持续时间，您随后将结合其他约束条件使用它。
对于自动停机功能，您知道按下信号的时间不能超过1秒，或5个时间步。因此，您想要确保驱动程序上下都是“真”或都是“假”在少于5步后按下。通过取驱动器中性点和检测器输出的AND，强制驱动器向下可以被按下的任何连续时间步长小于5的限制。
您还需要确保，在此期间，其他信号，如obstacle, EndStop和DriverUp不为真，因为这些信号将使控制器对下按做出响应。通过强制NOT(haldown)为真，使用Detector2捕获5个时间步骤。Detector2具有“Delayed Fixed Duration”输出类型。它还有“用于输入检测的时间步骤”= 5和“用于输出持续时间的时间步骤”= 1。
取这些构建的持续时间的AND。
对于AutoDown特性，您不希望限制控制器给出down命令的时间步长的数量。您知道，只要驾驶员没有再次按下向上或向下命令，或者没有撞到障碍物或窗框的物理端，控制器就会一直发出向下命令。此行为可以由Extender块捕获，该块具有“Infinite”扩展周期和一个外部复位信号，该信号对结束扩展的条件进行编码。
最后一部分是Implies块，它接受如上所述构造的时间持续时间，并检查控制器down命令对于该持续时间的每个时间步骤是否为真。
一旦你有了这个初始属性规范，你就可以用它来用Simulink Design Verifier进行属性验证。金宝app你会得到这个属性的反例。反例显示了这样一个场景:由于对先前检测到的障碍物作出响应，控制器处于紧急down状态，此时给出down命令。在添加约束以避免这种情况发生后，您将得到另一个反例:如果在之前给出up命令时按下了down按钮，则AutoDown功能将被禁用，只有在按下down按钮时才给出down命令。查看这些反例并观察模型，您可以看到一个模式，即只有当控制器处于中立状态时(即驾驶员按下按钮时)才启用AutoDown特性。
通过强制控制器输出为中立状态(up和down命令均为true)来合并此约束，作为AutoDown属性的先决条件。这个性质被证明是有效的。
%有效AutoDownopen_system (“sldvdemo_powerwindow_vs /验证Subsystem3”）
为属性验证生成测试用例
一旦属性被指定，除了属性证明之外，您还可以运行Simulink Design Verifier来自动生成测试用例，这些测试用例在属性中执行各种条件。金宝app这可以通过在属性的适当位置放置自定义Test Objective块来实现。
放置Test Objective块(带有“true”值)的一个这样的位置是在输入Implies块的第一个输入的信号上(如上面的属性所示)。在运行测试生成时，这个测试目标得到满足，并且您将得到一个测试用例，该测试用例将执行属性中编码的各种约束。金宝appSimulink Design Verifier还可以创建一个测试工具来模拟这个测试用例。带有相关信号的信号生成器模块如下所示。
现在可以模拟这个测试用例，并通过放置一个范围来显示两个Detector块和No_Cmd的输入和输出值，从而了解如何在属性中创建临时持续时间。
手动检查测试用例值使您能够查看指定的属性是否按照预期的行为。
这个Test Objective块有助于识别这样一个场景:属性是有效的，而Implies块不是简单地为真。当一个Implies块的输出为真，因为它的第一个输入为假时，它就为真。当您得到一个满足这个测试目标的测试用例时，您知道至少有一种情况是Implies块的第一个输入为真。
这个练习可以帮助您通过手动检查由Simulink Design Verifier自动生成的测试用例来验证您的属性规格。金宝app
清理
要完成这个示例，请关闭所有打开的模型。
close_system (“sldvdemo_TOBlocks”, 0);close_system (“sldvdemo_powerwindowController”, 0);close_system (“sldvdemo_powerwindow_vs”, 0);
你也可以从以下列表中选择一个网站:
