反推装置的属性证明工作流
此示例说明如何在反推装置设计模型中验证安全属性。该模型下方的 Properties 模块包含四个安全属性。Simulink® Design Verifier™ 会分析设计模型和安全属性,以证明正确性或识别反例。使用模型引用无需在设计模型中添加验证内容,使得验证内容可以独立于设计而存在。
open_system('sldvdemo_thrustrvs_verification');
此示例说明如何在反推装置设计模型中验证安全属性。该模型下方的 Properties 模块包含四个安全属性。Simulink® Design Verifier™ 会分析设计模型和安全属性,以证明正确性或识别反例。使用模型引用无需在设计模型中添加验证内容,使得验证内容可以独立于设计而存在。
open_system('sldvdemo_thrustrvs_verification');