电动车窗控制器时间属性

此示例展示了如何使用 Simulink® Design Verifier™ Temporal Operator 模块在电动车窗控制器模型中对时间系统需求模型，以进行属性证明和测试用例生成。

时间运算符

Simulink® Design Verifier™ 库提供了三个基本的时间操作符模块，可用于对时间属性模型。时间运算符的目的是支持时间需求的规范，使得建模的属性与实际的文本需求有更紧密的相关性。这些模块是用于构建更复杂的时间属性的低级构建模块。

电动车窗控制器

电动车窗控制器响应驾驶员和乘客的命令，发出上下移动车窗的指令。它还会对障碍物做出反应，并能从任一方向到达窗框的末端。

考虑电动车窗控制器的以下两个需求：

需求 1（障碍物响应）

一旦检测到障碍物，控制器应发出下降指令1秒。

需求 2（AutoDown 功能）

如果驾驶员按下下降按钮的时间少于 1 秒，控制器将持续发出下降命令，直到到达终点或驾驶员按下上升按钮。

%Model of the power window controller
open_system('sldvdemo_powerwindowController')
open_system('sldvdemo_powerwindowController/control')

属性规范

电动车窗验证系统是顶层模型，包含对电动车窗控制器模型的模型引用，指定控制器行为和建模需求。

%Model of the top-level verification system
open_system('sldvdemo_powerwindow_vs')

全球假设：电动车窗控制器是一个开放系统。这使得环境控制的输入、障碍物和终点（窗框的末端）可以自由发生。为了约束环境，为控制器模型添加两个全局假设。

1) 障碍物和终点停止位输入永远不会同时变为真。

2）在接下来的1秒区间内，障碍物没有出现多次。

对于障碍物的时间假设，使用输出类型为“延迟固定持续时间”的 Detector模块来捕获 1 秒的固定持续时间（5 个时间步长，0.2 个采样时间）。

% Global Assumptions
open_system('sldvdemo_powerwindow_vs/Global Assumptions')

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

% Obstacle Response
open_system('sldvdemo_powerwindow_vs/Verification Subsystem2')

这里，使用输出类型为“延迟固定持续时间”的 Detector模块作为属性规范。检测到障碍物后，构建4步固定区间。请注意，对于具有“延迟固定持续时间”输出类型的检测器，在输出构建阶段不会观察到输入。在没有假设的情况下，障碍物可以自由出现，您可能希望观察障碍物的所有中间发生情况。这可以通过具有 4 个时间步长的“有限”扩展持续时间的 Extender模块来实现。

现在考虑电动车窗控制器的AutoDown 功能。

为了说明起见，请考虑将此属性规范分为较小的部分：

第一个感兴趣的时间持续时间“驾驶员按下向下按钮的时间少于 1 秒”被 Detector1 捕获。在采样率为 0.2 时，1 秒区间被分解为 5 个时间步长。在检测到向下信号时，Detector1 在其输出处构建一个 5 步固定时间持续时间，随后您将把它与其他约束结合使用。
对于 AutoDown 功能，您知道向下信号不能按下超过 1 秒或 5 个时间步长。因此，您要确保按下向下按钮后，在少于 5 步的时间内，驱动器向上和向下按钮均为“真”或均为“假”。通过对该驾驶员中性状态和检测器输出进行 AND 运算，强制执行驾驶员向下约束，并且连续时间步长数不得超过 5 个。
您还需要确保在此期间，其他信号（例如障碍物、EndStop 和 DriverUp）不存在，因为这些信号会使控制器无法响应按下操作。这是使用 Detector2 捕获的，通过强制 NOT(HaltDown) 在 5 个时间步内为真。Detector2 具有“延迟固定持续时间”输出类型。它还具有“输入检测的时间步长”= 5 和“输出持续时间的时间步长”= 1。
对这些构建的持续时间进行 AND 运算。
对于自动下降功能，您不想限制控制器发出下降命令的时间步数。您知道，只要驾驶员没有再次按下向上或向下的命令，或者没有撞到障碍物或窗框的物理末端，您就希望控制器继续发出向下的命令。这种行为可以通过具有“无限”延长期和对结束延长的条件进行编码的外部复位信号的Extender模块来捕获。
最后部分是 Implies模块，它采用如上所述构建的时间持续时间并检查控制器关闭命令对于该持续时间的每个时间步是否为真。

一旦您有了这个初始属性规范，您就可以使用它来通过 Simulink Design Verifier 进行属性证明。您将得到此属性的一个反例。反例展示了这样一种场景：当控制器由于响应先前检测到的障碍物而处于紧急下降状态时，发出下降命令。添加约束以避免这种情况后，您将得到另一个反例：如果在先前发出向上命令时按下向下按钮，则自动向下功能将被禁用，并且只有在按下向下按钮时才会发出向下命令。通过查看这些反例并观察模型，您可以看到这样一种模式：只有当驾驶员按下向下按钮时，控制器处于中性状态，AutoDown 功能才会启用。

通过强制控制器输出为中性（无论是向上还是向下的命令都不正确）来纳入这一约束，作为 AutoDown属性的先决条件。此属性已被证明有效。

% Valid AutoDown
open_system('sldvdemo_powerwindow_vs/Verification Subsystem3')

属性验证的测试用例生成

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

放置 Test Objective模块（具有“真”值）的一个位置是输入到 Implies模块的第一个输入的信号上（如上面的属性所示）。在运行测试生成时，此测试目标得到满足，您将获得一个测试用例执行属性中编码的各种约束。Simulink Design Verifier 还可以创建一个测试框架来仿真这个测试用例。现在可以仿真这个测试用例，并通过放置一个显示两个 Detector 模块和 No_Cmd 的输入和输出值的范围来查看如何在属性中创建时间持续时间。

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

这个 Test Objective模块有助于识别属性有效而 Implies模块并非绝对正确的场景。当 Implies模块的输出为真时（因为其第一个输入为假），该模块显然为真。当您获得一个满足此测试目标的测试用例时，您就知道至少有一种情况，其中 Implies模块的第一个输入为真。

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

清理

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

close_system('sldvdemo_TOBlocks',0);
close_system('sldvdemo_powerwindowController',0);
close_system('sldvdemo_powerwindow_vs',0);

电动车窗控制器时间属性

时间运算符