形式验证

形式化验证有助于确认您的嵌入式系统软件模型和代码行为正确。形式化验证方法依赖于数学上严格的过程来搜索模型或代码的可能执行路径，以识别设计中的错误。您可以对模型、生成的代码和手工代码执行正式的验证。

模型的形式化验证

形式验证可以帮助您识别模型中的错误，并生成在模拟中重现错误的测试向量。与传统的测试方法不同，在传统的测试方法中，预期结果用具体的数据值表示，正式的验证技术让您可以继续工作系统行为模型．这样的模型可以包括测试场景和描述所需和不需要的系统行为的验证目标。形式化分析补充了模拟，并提供了对设计的更深入的理解。

详情见Simulink设计验证器™．

代码的正式验证

使用静态代码分析和形式化的验证方法，您可以使用工具来检测和证明在C/ c++或Ada编写的源代码中不存在溢出、除零、越界数组访问和其他运行时错误。您可以使用它们来执行手写或生成的嵌入式软件的代码验证。您还可以检查编码标准的遵从性，检查代码复杂度度量，并度量软件质量。

详细信息请参见Polyspace^®2022世界杯八强谁会赢？产品。