什么是规范模型？

自 R2022b 起

当您根据需求系统地验证模型时，您会为每个需求生成测试用例。这些测试验证了模型，您可以使用它来生成生产代码并建立模型满足需求的信心。为了创建满足您需求的测试，您可以构建一个规范模型。规范模型是一个可执行实体，您可以使用 Simulink^® Design Verifier™ 和 Requirements Toolbox™ 执行基于需求的测试。

如果您有一组用自然语言文本编写的需求，则可以使用 Requirements Table模块将它们表达为形式化需求。在一个或多个模块中定义需求之后，这些模块和信号就成为规范模型。与您想要测试的模型（称为设计模型）不同，规范模型仅指定要做什么，而不是如何做。

您可以使用规范模型来：

以系统和定量的方式验证一组需求。
实现基于需求的自动化测试。
确定您的设计模型和需求中的问题。

在基于需求的测试中使用规范模型

要创建和部署规范模型，请按照下列步骤操作：

编写需求--用自然语言文本写下您的需求，描述正在设计的系统的行为。直接在需求编辑器中创作它们或导入它们。有关进口需求的更多信息，请参阅从第三方应用程序导入需求。
构建规范模型--使用至少一个 Requirements Table模块规范模型设计为需求的正式表示。
链接需求- 您在 Requirements Table模块中创建的每个需求都会在需求编辑器中创建一个等效需求。请参阅配置正式需求的属性。将高级需求与规范模型的形式化需求联系起来。
分析完整性和一致性的形式化需求--手动识别不完整和不一致的需求集可能很困难。Requirements Table模块允许您自动分析这些问题的需求。请参阅识别不一致和不完整的正式需求集。
为规范模型生成测试 - 为每个需求生成至少一个测试，以证明其符合该需求。有关生成测试的更多信息，请参阅为子系统生成测试用例 (Simulink Design Verifier)。Simulink Design Verifier 根据 Requirements Table 模块中定义的需求自动创建测试目标。
将规范模型与设计模型连接起来--规范模型和设计模型通常不使用相同的输入和输出信号。通过在两个模型之间开发接口来转换您在步骤 5 中生成的测试用例。
开发设计模型- 使用需求开发设计模型。将需求与设计模型联系起来。
验证设计并分析覆盖率--在设计模型上运行步骤 5 中生成的测试，并验证结果是否符合规范模型和需求。生成覆盖率报告来识别缺失覆盖率，并根据需要细化需求。

此流程图说明了此过程。

This image shows the flowchart that illustrates the steps described in the previous list. The requirements are iteratively developed through the first four steps, and the design model and specification model are

构建规范模型

考虑使用规范模型进行基于需求的测试中描述的自动驾驶仪控制器模型。在此示例中，您将开发包含定义输出的逻辑与时序条件的需求。

识别规范模型接口

列出与您要测试的需求相关的规范模型的输入和输出信号。忽略需求未指定且不影响测试输出的信号。在此示例中，需求指定五个输入和两个输出。规格模型输入信号为：

自动驾驶仪接合开关--用于启用或禁用自动驾驶仪控制器的开关
航向接合开关 - 当自动驾驶仪仪开关接合时，指定自动驾驶仪控制器模式的开关
滚转引用目标旋钮--将所需的滚转角度值传送给自动驾驶仪控制器的旋钮
航向引用转动旋钮--为航向模式提供设定点值的旋钮
飞机滚转角--飞机当前的滚转角度

输出信号为：

副翼指令--副翼执行器的输出
滚转引用命令--显示窗口上的输出指示副翼执行器的设定值

确定每个需求的预条件、后条件和操作

对于需要验证的需求，将文本需求转化为可以表示为预条件、后条件和动作的逻辑表达式。您可以将形式化需求定义为预条件、后条件和操作的组合：

先决条件--在评估其余需求之前，必须在指定时间内成立的条件
后条件 - 如果相关先决条件在指定时间内成立，则该条件必须成立
动作 - 如果相关先决条件在指定时间内成立，则必须执行的行为

您可能会发现某些需求可以交替使用后条件或操作，或者同时使用后条件和操作。根据您的设计模型的配置指定您想要使用哪一个。

例如，考虑这个指定自动驾驶仪控制器模式的高级需求：

自动驾驶仪控制器模式由以下因素决定：

当自动驾驶仪接合开关未接合时，自动驾驶仪控制器处于关闭状态。
当自动驾驶仪接合开关接合且航向接合开关未接合时，自动驾驶仪控制器为 ROLL_HOLD_MODE。
当自动驾驶仪接合开关和航向接合开关同时接合时，自动驾驶仪控制器为 HDG_HOLD_MODE。

您可以将这些需求写成以下逻辑表达式：

需求	预条件	动作
`1`	`AP_Engage_Switch == false`	`Mode = Off`
`2`	`AP_Engage_Switch == true && HDG_Engage_Switch == false`	`Mode = ROLL_HOLD_MODE`
`3`	`AP_Eng_Switch == true && HDG_Engage_Switch == true`	`Mode = HDG_Hold_Mode`

对其余需求重复此过程。

确定需求中的设计价值表达

您的需求可能会指定设计模型必须满足的值的范围，或者您可能希望参数化您在每个需求中评估的值。这些值并不总是能够轻易地用文字值来描述。您可以使用 Requirements Table模块将表达式中的值表示为常量或参数数据。请参阅在 Requirements Table 模块中定义数据。您可以在整个仿真中更改数据。除了为数据分配数值之外，该模块支持其他数据类型，例如字符串，枚举或范围。使用适合您需要的值的表示。

在自动驾驶仪控制器模型中，需求指定飞机滚转角度的阈值。这张图说明了阈值的数值和文字对应关系。

This image shows the roll angle values and ranges that correspond to the high-level representation of the design values.

创建 Requirements Table 模块

在确定了想要在形式化需求中使用的信号表示、值和表达式之后，分别在每个需求的预条件 后条件和操作列中写下预条件、后条件和操作的逻辑表达式。如果您的需求有子项或依赖项，您可以将这些关系包含在模块中。请参阅在 Requirements Table 模块中建立层次结构。

您在 Requirements Table模块中创建的每个需求都会在需求编辑器中创建一个等效需求。在编辑器中更新需求的附加文本属性，例如描述。请参阅配置正式需求的属性。

在自动驾驶仪控制器模型中，规范模型包括两个Requirements Table模块。AP_Mode_Determination定义了自动驾驶仪控制器模式的形式化需求。

This image shows the requirements for the autopilot controller mode. It contains three requirements that are derived from the plain text requirements in the example model.

另一个 Requirements Table模块Cmd_Determination 描述了副翼命令和滚转引用命令的期望输出。

This image shows the requirements for the autopilot commands. It contains requirements that are derived from the plain text requirements in the example model.

最终规范模型

将 Requirements Table 模块连接到输入、输出和彼此之后，最终的规范模型为：

This image shows the final specification model.

准备测试生成的规范模型

Simulink Design Verifier 根据 Requirements Table 模块中定义的需求自动创建测试目标。如果需要约束测试目标的值，您可以在信号源中指定它们，或者将它们包含在模块的假设表中。请参阅将假设添加到需求中。为了准备用于测试生成的规范模型，请设置模型覆盖率目标。在 Design Verifier 选项卡的准备部分中，点击测试生成设置。在配置参数窗口中，展开 Design Verifier 列表并点击测试生成。将模型覆盖率目标设置为最能捕获所需覆盖率的选项。