基于模型的设计验证器

Natick, ma -基于模型的设计方法允许嵌入式系统的开发人员——特别是安全关键或复杂设计的开发人员——自动获得测试用例，以满足行业标准度量，例如修改条件/决策覆盖(MC/DC)，同时在开发过程的早期发现设计错误，当它们的修复成本显著降低时。仿真是基于模型设计的一项关键活动，它使工程师能够深入了解系统行为，调整参数以获得最佳性能，并确保他们的设计符合预期。
的MathWorks”Simulink设计验证器，它使用来自Prover Technology的Prover插件为Simulink和Stateflow模型生成测试并证明设计属性，通过基于形式化方法的验证和确认技术来增强仿真，这大大减少了为建立完整的模型覆盖率和验证需求而手工编写测试代码的需要。工程师可以生成满足标准覆盖目标以及用户定义的测试目标和需求的测试输入。这些测试输入也可以与使用测量数据定义的测试相结合，这样模拟就可以针对模型覆盖需求和真实场景进行测试。
对于属性证明，工程师可以直接捕获设计需求和性能目标，作为Simulink或Stateflow模型中的属性。Simulink设计验证器用数学方法证明这些特性是否满足，如果不满足，则提供违反这些特性的反例。因此，工程师可以发现设计缺陷、未满足的需求以及难以到达的状态或逻辑，这些都很难单独使用仿真来发现。
The MathWorks设计自动化市场总监Paul Barnard说:“基于模型的设计正广泛应用于嵌入式系统开发，从研发和概念验证项目进入生产程序。”随着这种转变，客户对验证、验证和测试工具的需求日益迫切，而Simulink设计验证器可以帮助解决这些问题。”
该软件集成了来自Prover Technology的Prover插件证明引擎，可以自动生成测试用例和反例。它还通过使用自动数学推理来探索模型执行路径来执行证明。这种系统的分析补充了仿真，并提供了对设计行为的更深入的了解。
“我们与The MathWorks密切合作，扩展了我们的Prover插件接口，以处理通常在Simulink和Stateflow中建模的动态系统，”Prover Technology首席营销官Marcus Tallhamn说。“我们很自豪能够成为嵌入式系统开发人员在没有正式方法专业知识的情况下执行最先进的正式验证工具的一部分。”
Simulink Design Verifier可立即用于Microsoft Windows和Linux平台。美国的标价从8000美元起。
- - - - - -编辑C.G.马西，高级编辑

您是否具有本内容中提到的主题的经验和专业知识?您应该考虑为我们的CFE媒体编辑团队做出贡献，并获得您和您的公司应得的认可。点击在这里开始这个过程。