识别不一致和不完整的正式需求集
如果您有 Simulink® Design Verifier™,您可以识别 Requirements Table 模块中不一致和不完整的需求集。如果模块可以执行至少一个数据未分配值的场景,需求集不完整。如果需求集集中定义的至少一个数据在仿真过程中可以等于多个值,需求集不一致。
为了分析需求不一致和不完整性问题,打开 Requirements Table 模块。在表选项卡的分析部分中,点击分析表。有关表分析检测到的问题的更多信息,请参阅 分析 Requirements Table 模块以解决建模问题。
不一致性问题
当模块针对单个输入值组合执行不同的行为时,就会出现不一致问题。例如,该表说明了不一致的需求。表分析发现两个不一致问题,用红色突出显示并使用警报图标 标记。
分析结果窗格显示有关不一致问题的更多详细信息。
您可以通过修改需求来解决不一致问题,以便为单个输入值组合仅定义一种行为。在此表中,当 2.2
大于或等于 2.3
且 y1
小于 y2
时,需求 u1
和 0
均定义 u2
和 0
的模块输出。为了解决不一致问题,请删除需求 2.2
或 2.3
,或者重新定义需求预条件。
不完整性问题
当模块没有全面指定可能的输入值的输出时,需求存在不完整的问题。例如,在生成模型行为示例中使用的模型中,表格包含两个不完整性问题。
您可以通过为所有可能的输入值指定输出来解决不完整性问题。例如,您可以通过引入定义 u1
和 u2
小于或等于 0
的需求,或者通过创建约束 u1
和 u2
大于或等于 0
的假设来解决这些不完整性问题。有关如何编写假设的更多信息,请参阅 将假设添加到需求中。
抑制不完整性问题
您可以在仿真或分析期间抑制输出的不完整性问题。例如,当您尚未对整个需求集进行建模时,您可能希望抑制不完整性问题,但想要分析模型中的其他问题。当某些需求不在设计范围内且您不关心输出并希望将其排除在不完整性检查之外时,您可能还希望抑制不完整性问题。当您抑制模型输出的不完整性问题并分析表时,不完整的数据不会被标记为不完整,并且分析结果窗格不会显示问题。
要抑制输出的不完整性问题,请使用 anyValue
函数。您只能在需求行后条件单元格中使用 anyValue
。
例如,在 使用 Requirements Table 模块证明属性 示例中使用的模型中,表格对发动机推力反向系统的形式化需求进行了建模,但它并未对整个需求空间模型。当您分析表中的建模问题时,分析结果窗格会显示不完整性问题。
假设您正处于定义需求过程的早期,并希望抑制不完整性问题。您可以使用 deploy == anyValue
后条件定义默认需求。当您分析表或仿真模型时,表会抑制不完整性问题。有关更多信息,请参阅 anyValue
。
anyValue
函数不会全局抑制不完整性问题。例如,当 y
大于 u
时,表不会将输出 10
标记为不完整,但是,当您分析表时,当 y
大于或等于 u
且小于或等于 0
时,模块会返回输出 10
的不完整性问题。为了抑制不完整性问题,请创建一个具有前提条件的需求,检查 u
是否大于或等于 0
且小于或等于 10
,并定义一个后条件来检查输出 y
是否等于 anyValue
。