财产证明巡航控制的工作流

开放的例子

这个例子展示了如何找到一个财产违反使用仿真软件®设计校验™财产证明的分析。万博1manbetx您作为属性模型的安全需求,然后验证设计模型与需求。

当您执行财产证明分析、仿真软件设计验证器生成一个反例,你使用调试属性违反。万博1manbetx

的sldvdemo_cruise_control_verification模型包含一个参考模型sldvdemo_cruise_control_defective设计模型。设计模型是一个巡航控制系统,由一个比例积分控制器计算油门输出基于实际和目标速度之间的差异。

open_system (“sldvdemo_cruise_control_verification”);

安全属性的油门输出建模安全属性断言验证子系统的块。

open_system (“sldvdemo_cruise_control_verification /安全属性”);

在设计验证器选项卡上,单击证明属性。

窗口分析完成后,结果总结报告,一个目标是伪造的。

利用模型和信号生成器生成对话框打开,显示了反例。

在信号生成器对话框中,单击开始模拟按钮▸。

诊断查看器窗口会显示一个错误,指出仿真终止是因为断言发生在时间0.04。

可选地,您可以调试属性违反使用模型切片机。有关更多信息,请参见通过使用模型切片机调试侵犯财产证明。

错误的行为表现出的反例是固定的sldvdemo_cruise_control_verification_fixed模型。

open_system (“sldvdemo_cruise_control_verification_fixed”);

房地产证明工作流,您可能需要重新设计系统和/或重新定义属性和执行这样的迭代。

打开引用模型sldvdemo_cruise_control_fixed并打开控制器子系统。在这个子系统,设计模型更新重置油门当积极主动控制输出。

在设计验证器选项卡上,单击证明属性。窗口分析完成后,结果总结报告,目的是有效的。