来自系列:在DO-178C开发过程中使用合格工具
比尔波特,Mathworks
显示源代码的准确性和一致性是DO-178C的目标。使用正式方法时,DO-333允许通过正式分析满足这些目标。PolySpace Code Prover™是一种工具,可以使用抽象解释对C源代码进行正式分析。PolySpace代码递文检测到源代码中的某些潜在的运行时间错误。可以在源代码中检测到的错误类型:未到达代码或函数未调用,数字溢出,逐个划分,浮点数无效操作,无效的移位操作,非法解密的指针,非终止呼叫或循环,以及ob-of绑定数组索引。可以在单个分析运行中分析这些检查,并为这些潜在错误生成组合报告。此报告还清楚地显示了可能发生特定错误的代码行。该报告使用颜色编码方案来指示每行代码的状态:绿色表示该行代码中没有错误,灰色表示无法访问的代码行,红色表示已被证明具有错误的代码和橙色指示可能需要进一步的手动分析的可能错误。DO资格套件为PolySpace代码抄本提供必要的工件,以限定运行时错误检测和报告。 The kit also provides the evidence necessary to show soundness of the formal method, as required by DO-333.
您还可以从以下列表中选择一个网站:
选择中国网站(以中文或英文)以获取最佳网站性能。其他MathWorks国家网站未优化您的位置。