证明模型中的属性
关于此示例
以下部分描述了 Simulink®模型,您可以证明该模型使用 Proof Objective模块指定的属性。此示例演示了Simulink Design Verifier™的属性证明功能。
在此示例中,您执行以下任务。
构建示例模型
构建一个Simulink模型用于本例中:
创建一个空的Simulink模型。
将以下模块复制到空白模型窗口中:
从 Sources 库中,一个 Inport模块用于启动输入信号,其值 Simulink Design Verifier 控制
来自逻辑和位运算库,一个 Compare To Zero模块提供简单的逻辑
来自 Sinks 库的 Outport模块用于接收输出信号
连接这些模块,使您的模型看起来类似于以下模型:
在 建模 选项卡上,点击模型设置 。
在配置参数对话框的 求解器窗格中的 求解器选择 中:
将 类型 选项设置为 定步长 。
将 求解器 选项设置为 离散(无连续状态) 。
Simulink Design Verifier 只能分析使用固定步长求解器的模型。
单击“OK”保存更改并关闭“配置参数”对话框。
使用名称
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模块的信号对于它接收到的任何信号始终达到该值。
单击“OK”应用更改并关闭“Proof Objective ”模块参数对话框。
保存您的模型并保持打开状态。
配置属性证明选项
配置 Simulink Design Verifier 来证明您所检测的 ex_property_proving_example_basic
模型的属性:
打开
ex_property_proving_example_basic
模型。在 Design Verifier 选项卡的 模式 部分中,选择 属性证明 。
点击 Property Proving Settings 。
单击“OK”应用更改并关闭“配置参数”对话框。
注意
在 属性证明窗格上,您可以选择指定其他参数的值,这些参数控制 Simulink 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 结果窗口始终是最顶层的可见窗口。要允许窗口移动到其他窗口后面,点击 并清除 Always on top 。
单击突出显示的Proof Objective模块。
Simulink Design Verifier 结果窗口表明,比较到零的输出信号不是 1 这一证明目标已被反例所推翻。
查看详细分析报告
要创建详细的 HTML 分析报告:
在Simulink Design Verifier结果摘要窗口中,点击生成详细的分析报告。
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
的框架模型。框架模型包含以下项目:
双击输入模块。
输入信号 1 导致比较零模块的输出为 0。这个反例违反了规定“比较到零”模块的输出为 1 的证明目标。
用反例仿真模型
仿真框架模型来观察模型中证伪证明目标的反例:
打开
ex_property_proving_example_basic
模型。在 仿真 选项卡上,点击库浏览器 。
从 Sinks 库中,将 Scope模块复制到您的框架模型窗口中。Scope模块允许您查看模型中 Compare To Zero模块输出的信号值。
在您的框架模型窗口中,将测试单元子系统的输出信号连接到 Scope模块。
要仿真您的框架模型,请在“仿真”选项卡上点击“运行”。
Simulink软件仿真了框架模型。
在线框架模型窗口中,双击 Scope模块以打开其显示窗口。
Scope模块显示模型中 Compare To Zero模块输出的信号值。在这个例子中,Compare To Zero模块在整个仿真中返回 0(假),这使得比较到零模块的输出为 1(真)的证明目标变得错误。Signal Builder模块提供的反例证明目标被证伪了。
查看分析结果
只要您的模型保持打开,您就可以在结果摘要窗口中查看最近的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模块复制到您的模型。
在模型窗口中,将 Proof Assumption模块插入 Inport 和 Compare To Zero 模块之间。
在您的模型中,双击Proof Assumption模块以访问其属性。
Proof Assumption模块参数对话框打开。
在 值 框中,输入
[-1, 0]
。在证明该模型的属性时,Simulink Design Verifier将进入Compare To Zero模块的信号值限制在指定的范围内。如果“比较到零”模块的输入始终在此范围内,则“比较到零”模块的输出将始终为 1。单击“应用”,然后单击“OK”以应用更改并关闭“Proof Assumption”模块参数对话框。
保存
ex_property_proving_example_basic
模型并保持打开。
重新分析示例模型
分析您修改的模型,看看Proof Assumption模块如何影响属性证明分析。
打开ex_property_proving_example_basic
模型。在 Design Verifier 选项卡上,点击证明属性 。
分析完成后,日志窗口会显示选项。没有创建框架模型的选项,因为分析满足了模型中的所有证明目标,所以没有反例。
审查第二次分析的结果
回顾第二次分析的结果:
审查模型结果
突出显示模型以查看分析结果:
点击 在模型上突出显示分析结果 。
证明目标现在以绿色突出显示。
单击Proof Objective模块。
Simulink Design Verifier 结果窗口显示,声明信号为 1 的证明目标是有效的。
查看分析报告
在详细报告中查看分析结果:
点击 生成详细的分析报告 。
在 目录 中,点击
Summary
。摘要章节表明Simulink Design Verifier在模型中证明了一个证明目标。
约束部分列出了您在 Proof Assumption模块中指定的分析约束。
滚动回到浏览器窗口的顶部。在 目录 中,点击
Proof Objectives Status
。目标已证明有效表列出了Simulink Design Verifier已证明有效的证明目标。
向下滚动以查看“属性”章节或转到浏览器窗口顶部,然后在 目录 中点击
Properties
。证明目标摘要表明 Simulink Design Verifier 证明了您在模型中指定的目标。Proof Assumption模块将输入信号的范围限制在区间[-1, 0] 内。因此,软件证明该区间不包含大于零的值,从而满足证明目标。
分析矛盾的模型
如果分析产生错误The model is contradictory in its current configuration
,则表示软件检测到模型中存在矛盾,因此无法分析该模型。如果您的模型具有带有不正确参数的 Proof Assumption 模块,则可能会产生矛盾。例如,假设当信号为常数 10 时,信号必须介于 0 和 5 之间。
如果软件检测到矛盾,所有先前的结果将无效,并且软件将报告所有属性都是伪造的。
注意
通过设计最小值/最大值或测试条件/证明假设在输入处添加的约束不会导致矛盾。但是,如果使用测试条件/证明假设约束计算下游的信号,则必须确保约束条件通过模型计算是可行的。否则,得到的模型是矛盾的,可能会产生无效的结果,无论是否存在明显的分析错误。为了确保约束可行,首先使用测试目标尝试相同的条件。如果可以满足,则可以安全地使用相同的条件作为约束。
在大型模型中证明属性
要彻底证明你的模型,需要Simulink Design Verifier搜索模型所有可达的配置 — — 即使是那些需要经过很长时间才能达到的配置。完全搜索模型所需的计算时间和内存通常会使详尽的证明变得不切实际。
证明大型模型中的属性 给出了有关可用于提高大型模型的属性证明分析的性能的策略的详细信息。