显示低层次需求和软件架构的准确性和一致性是DO-178C的一个目标。当使用形式化方法时，DO-333允许通过形式化分析来满足这些目标，可以在使用模型进行设计时应用形式化分析。金宝appSimulink Design Verifier™是一个可以在Simulink上执行形式化分析的工具®和Stateflow®模型。Simulink Design Verifier的形式化分析特性之一是设计错误金宝app检测，它可以检测设计模型中某些潜在的运行时错误。在模型中可以检测到的错误类型有:死逻辑、整数溢出、除零、超过指定的信号最小值和最大值，以及出界数组访问。对死逻辑的分析必须与其他缺陷分开进行。将为模型生成一个死逻辑报告，并将指出模型中具有不可到达逻辑的任何区域，从而指出设计错误。该报告将清楚地显示作为死逻辑一部分的模型元素。其他可能的缺陷都可以在一个单独的分析运行中进行分析，并为那些潜在的错误生成一个联合报告。该报告还清楚地显示了可能发生特定错误的模型元素。DO确认套件提供了必要的工件，以确认Simulink设计验证器的设计错误检测和报告。金宝app该工具包还提供了必要的证据，以证明正式方法的可靠性，如DO-333所要求的那样。
