证明模型中的属性
关于此示例
以下部分描述了 Simulink® 模型，您可以证明该模型使用 Proof Objective 模块指定的属性。此示例演示了 Simulink Design Verifier™ 的属性证明功能。
在此示例中，您执行以下任务。
构建示例模型
构建一个 Simulink 模型用于本例中：
创建一个空的 Simulink 模型。
将以下模块复制到空白模型窗口中：
从 Sources 库中，一个 Inport 模块用于启动输入信号，其值 Simulink Design Verifier 控制
来自逻辑和位运算库，一个 Compare To Zero 模块提供简单的逻辑
来自 Sinks 库的 Outport 模块用于接收输出信号
连接这些模块，使您的模型看起来类似于以下模型：
在建模选项卡上，点击模型设置。
在“配置参数”对话框的求解器窗格中的求解器选择中：
将类型选项设置为定步长。
将求解器选项设置为离散(无连续状态)。
Simulink Design Verifier 只能分析使用固定步长求解器的模型。
点击确定保存更改并关闭“配置参数”对话框。
使用名称
ex_property_proving_example_basic保存您的模型。
检查示例模型的兼容性
每次 Simulink Design Verifier 软件分析模型时，在分析开始之前，软件都会执行兼容性检查。如果您的模型不兼容，软件将无法分析它。
您还可以在开始分析之前确保您的模型与 Simulink Design Verifier 兼容：
打开
ex_property_proving_example_basic模型。在 Design Verifier 选项卡上，点击检查兼容性。
Simulink Design Verifier 软件显示日志窗口，说明您的模型是否兼容。
您刚刚创建的模型是兼容的。
如果模型部分兼容怎么办？
如果兼容性检查表明您的模型部分兼容，则您的模型至少包含一个 Simulink Design Verifier 不支持的对象。您可以分析部分兼容的模型，但默认情况下，不受支持的对象将被删除。分析结果可能不完整。有关自动插桩的详细信息，请参阅 使用自动插桩处理不兼容问题。
仪器示例模型
准备您的示例模型，以便您可以使用 Simulink Design Verifier 证明其属性。具体来说，通过添加和配置 Proof Objective 模块来检测模型：
在 MATLAB® 命令窗口中，输入
sldvlib。出现 Simulink Design Verifier 库。
打开目标和约束子库。
将 Proof Objective 模块复制到您的模型并将其插入到 Compare To Zero 和 Outport 模块之间。
在您的模型中，双击 Proof Objective 模块。
将打开 Proof Objective 模块参数对话框。
在值框中，输入
1。Simulink Design Verifier 软件将尝试证明 Compare To Zero 模块的信号对于它接收到的任何信号始终达到该值。
点击确定应用更改并关闭“证明目标”模块参数对话框。
保存您的模型并保持打开状态。
配置属性证明选项
配置 Simulink Design Verifier 来证明您所检测的 ex_property_proving_example_basic 模型的属性：
打开
ex_property_proving_example_basic模型。在 Design Verifier 选项卡的模式部分中，选择属性证明。
点击 Property Proving Settings。
点击确定应用更改并关闭“配置参数”对话框。
注意
在属性证明窗格上，您可以选择指定其他参数的值，这些参数控制 Simulink Design Verifier 如何证明模型的属性。有关详细信息，请参阅 Design Verifier 窗格：属性证明。
保存
ex_property_proving_example_basic模型。
分析示例模型
要分析 ex_property_proving_example_basic 模型，请在 Design Verifier 选项卡上点击证明属性。Simulink Design Verifier 开始属性证明分析。
在分析过程中，日志窗口显示分析的进度。它显示已处理的目标数量以及哪些目标得到满足或被证伪等信息。
要随时终止分析，请在日志窗口中点击停止。
查看分析结果
分析完成后，日志窗口将显示以下选项以供查看结果：
突出显示模型上的分析结果
生成详细的 HTML 分析报告
使用测试用例创建框架模型
仿真模型创建的测试用例并生成模型覆盖率报告
您还可以查看 Simulink Design Verifier 数据文件。有关数据文件的详细信息，请参阅管理 Simulink Design Verifier 数据文件。
以下部分介绍如何查看分析结果：
审查模型结果
您可以通过查看模型窗口中突出显示的模块来一目了然地查看分析结果。突出显示可以有四种颜色：
绿色 - 分析证明所有证明目标均有效。
红色 - 分析推翻了证明目标，并生成了证伪该目标的反例。
橙色 - 分析推翻了证明目标，但无法生成反例或证明目标仍未确定。出现此结果的原因是：
软件无法控制其值的信号的证明目标，例如 Constant 模块
依赖于非线性计算的证明目标
产生算术错误（如除以零）的证明目标
启用自动插桩，并且分析遇到不受支持的模块，它不理解该模块的操作，但分析需要生成反例
分析超时
分析引擎的局限性
灰色 - 模型对象不是分析的一部分。
突出显示示例模型上的分析结果：
在
ex_property_proving_example_basic分析的结果摘要窗口中，点击在模型上突出显示分析结果。
Proof Objective 模块以红色突出显示，这表明证明目标被反例证伪。
出现 Simulink Design Verifier 结果窗口。
当您点击模型中的对象时，此窗口将发生变化，显示该对象的详细分析结果。
提示
默认情况下，Simulink Design Verifier 的“结果”窗口始终是最顶部的可见窗口。要允许窗口移动到其他窗口后面，点击
并清除始终在顶部。点击突出显示的 Proof Objective 模块。
Simulink Design Verifier 结果窗口表明，比较到零的输出信号不是 1 这一证明目标已被反例所推翻。
查看详细分析报告
要创建详细的 HTML 分析报告：
在 Simulink Design Verifier 结果摘要窗口中，点击 HTML 查看详细分析报告。
HTML 报告将在浏览器窗口中打开。
该报告包括以下内容目录。点击超链接可以导航至报告中的特定部分。
在目录中，点击
Summary。
摘要概述了分析结果，并表明 Simulink Design Verifier 发现了一个反例，该反例证明了模型中的目标。
在目录中，点击
Proof Objectives Status。
通过反例证伪的目标表列出了 Simulink Design Verifier 使用其生成的反例所反驳的证明目标。您可以通过点击
Proof Objective在模型窗口中找到目标；软件会在模型窗口中突出显示相应的 Proof Objective 模块。在用反例证伪的目标表中，在反例列下，点击
1。
本节显示有关证明目标 1 的信息，并提供有关 Simulink Design Verifier 生成的用于反驳该目标的反例的详细信息。在这个反例中，信号值 99 证明您使用 Proof Objective 模块指定的目标不成立。也就是说，99 不小于或等于 0，这导致 Compare To Zero 模块返回 0（假）而不是 1（真）。
审查框架模型
创建一个带有反例的框架模型，以证伪模型中的证明目标：
在 Simulink Design Verifier 日志窗口中，点击创建框架模型。
该软件创建一个名为
ex_property_proving_example_basic_harness的框架模型。
框架模型包含以下模块：
双击
Inputs模块。打开“模块参数”对话框。点击打开信号编辑器按钮，打开信号编辑器对话框。
输入信号 1 导致比较零模块的输出为 0。这个反例违反了规定“比较到零”模块的输出为 1 的证明目标。
用反例仿真模型
仿真框架模型来观察模型中证伪证明目标的反例：
打开
ex_property_proving_example_basic模型。在仿真选项卡上，点击库浏览器。
从 Sinks 库中，将 Scope 模块复制到您的框架模型窗口中。Scope 模块允许您查看模型中 Compare To Zero 模块输出的信号值。
在您的框架模型窗口中，将
Test Unit子系统的输出信号连接到 Scope 模块。
仿真框架模型。
在线框架模型窗口中，双击 Scope 模块以打开其显示窗口。
Scope 模块显示模型中 Compare To Zero 模块输出的信号值。在这个例子中，Compare To Zero 模块在整个仿真中返回 0（假），这使得比较到零模块的输出为 1（真）的证明目标变得错误。Signal Editor 模块提供的反例证明目标被证伪了。
查看分析结果
只要您的模型保持打开，您就可以在结果摘要窗口中查看最近的 Simulink Design Verifier 分析结果。
在 Design Verifier 选项卡的查看结果部分中，点击结果摘要。“结果摘要”窗口打开，显示最新的 Simulink Design Verifier 分析的结果。
对于任何 Simulink Design Verifier 分析，您都可以从“结果摘要”窗口执行这些任务。
| 任务 | 了解详细信息 |
|---|---|
在模型上突出显示分析结果。 | 突出显示模型结果 |
生成详细分析报告。 | 查看结果 |
创建框架模型，或者在框架模型已经存在的情况下打开它。 如果在分析过程中没有创建反例，则此选项不可用。 | 管理 Simulink Design Verifier 框架模型 |
查看数据文件和日志文件。 | 管理 Simulink Design Verifier 数据文件 |
关闭模型后，您将无法再查看分析结果。
自定义示例证明
修改简单的 Simulink 模型，其证明目标 Simulink Design Verifier 在上一个任务中被推翻。具体来说，通过添加和配置 Proof Assumption 模块来自定义证明：
在 MATLAB 命令窗口中，输入
sldvlib。Simulink Design Verifier 库打开。
打开目标和约束子库。
将 Proof Assumption 模块复制到您的模型。
在 Inport 和 Compare To Zero 块之间插入 Proof Assumption 模块。
双击 Proof Assumption 模块来访问其属性。
打开“模块参数”对话框。
在值框中，输入
[-1, 0]。在证明该模型的属性时，Simulink Design Verifier 将进入 Compare To Zero 模块的信号值限制在指定的范围内。如果“比较到零”模块的输入始终在此范围内，则“比较到零”模块的输出将始终为 1。点击应用，然后点击确定以应用更改并关闭“模块参数”对话框。
保存
ex_property_proving_example_basic模型并保持打开。
重新分析示例模型
分析您修改的模型，看看 Proof Assumption 模块如何影响属性证明分析。
打开 ex_property_proving_example_basic 模型。在 Design Verifier 选项卡上点击证明属性。
分析完成后，日志窗口会显示选项。没有创建框架模型的选项，因为分析满足了模型中的所有证明目标，所以没有反例。
审查第二次分析的结果
回顾第二次分析的结果。
审查模型结果
突出显示模型以查看分析结果：
点击在模型上突出显示分析结果。
证明目标现在以绿色突出显示。
点击 Proof Objective 模块。
Simulink Design Verifier 结果窗口显示，声明信号为 1 的证明目标是有效的。
查看分析报告
在详细报告中查看分析结果：
点击生成详细的分析报告。
在目录中，点击摘要。
摘要章节表明 Simulink Design Verifier 在模型中证明了一个证明目标。
滚动到约束部分。约束部分列出了您在 Proof Assumption 模块中指定的分析约束。
滚动回到浏览器窗口的顶部。在目录中，点击测试目标状态。
目标已证明有效表列出了 Simulink Design Verifier 已证明有效的证明目标。
向下滚动以查看“属性”章节，然后在目录中点击属性。
证明目标摘要表明 Simulink Design Verifier 证明了您在模型中指定的目标。Proof Assumption 模块将输入信号的范围限制在区间[-1, 0] 内。因此，软件证明该区间不包含大于零的值，从而满足证明目标。
分析相互矛盾的模型
如果分析产生错误 The model is contradictory in its current configuration，则表示软件检测到模型中存在矛盾，因此无法分析该模型。如果您的模型具有带有不正确参数的 Proof Assumption 模块，则可能会产生矛盾。例如，假设当信号为常数 10 时，信号必须介于 0 和 5 之间。
如果软件检测到矛盾，所有先前的结果将无效，并且软件将报告所有属性都是伪造的。
注意
通过设计最小值/最大值或测试条件/证明假设在输入处添加的约束不会导致矛盾。但是，如果您使用测试条件/证明假设来约束计算下游的信号，则必须确保约束条件通过模型计算是可行的。否则，得到的模型是矛盾的，可能会产生无效的结果，无论是否存在明显的分析错误。为了确保约束可行，首先使用测试目标尝试相同的条件。如果可以满足，则可以安全地使用相同的条件作为约束。
在大型模型中证明属性
要彻底证明您的模型，需要 Simulink Design Verifier 搜索模型所有可达的配置 - 即使是那些需要经过很长时间才能达到的配置。完全搜索模型所需的计算时间和内存通常会使详尽的证明变得不切实际。
证明大型模型中的属性 给出了有关可用于提高大型模型的属性证明分析的性能的策略的详细信息。
