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