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

模型的形式验证

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

有关详情请参阅金宝appSimulink设计验证器™。

代码的形式验证

运用静态代码分析和形式验证方法中，可以使用工具除以零检测和证明不存在溢出的，外的界定数组访问，并且在用C / C ++或阿达源代码以外的运行时错误。你可以用它们来执行手写验证代码或生成嵌入式软件。您还可以检查是否符合编码标准，审查代码复杂度指标，并衡量软件质量。

有关详细信息，请参阅Polyspace^®下载188bet金宝搏产品。