使用 Polyspace Code Prover 进行源代码验证
Polyspace 验证的工作原理
Polyspace® 软件使用静态验证来证明没有运行时错误。静态验证可在不实际执行程序的情况下获取程序的动态属性。这与其他技术(如运行时调试)有很大不同,因为它提供的验证不是基于给定的测试用例或测试用例集。在 Polyspace 验证中获得的动态属性适用于软件的所有执行情况。
什么是静态验证
静态验证是一个广义的术语,适用于任何无需执行程序即可获得程序动态属性的工具。不过,大多数静态验证工具仅在搜索可能存在潜在错误的构造时验证软件的复杂度。而 Polyspace 验证则提供了深度验证,可识别绝大部分运行时错误以及与全局共享数据之间可能的访问冲突。
Polyspace 验证通过使用软件操作和数据的典型逼近值来逼近被验证的软件。
以如下代码为例:
for (i=0 ; i<1000 ; ++i) { tab[i] = foo(i); }
要检查变量 i
从未溢出 tab
的范围,传统方法是枚举 i
的每个可能值。这需要进行 1000 次检查。
利用静态验证方法,变量 i
可通过其定义域变化模型来表示。例如,i
的模型可表示为该变量属于静态区间 [0..999]。(根据数据的复杂度,也可以使用凸多面体、整数格和更精细的模型来实现此目的)。
根据定义,逼近模型会导致信息丢失。例如,循环中每周期 i
会递增 1 这一信息会丢失不过重要的是,我们并不需要这一信息来确保不会发生范围错误;只需证明 i
的定义域变化小于 tab
的范围即可。只需进行一次检查即可确定这一点,因此与传统方法相比,效率会有所提高。
静态代码验证有一个精确解。但这个精确解并不切实际,因为它需要枚举所有可能的测试用例。因此,对于实用的工具,只需要求逼近解。
穷尽性
在穷尽性方面没有任何损失。原因是 Polyspace 验证是通过执行上限逼近来实现的。换句话说,计算出的程序变量变化域是其实际变化域的超集。因此,Polyspace 会验证需要检查的运行时错误项。
PolyspaceCode Prover 验证的值
Polyspace 验证可以帮助您实现以下目标:
提高软件可靠性
Polyspace 软件通过证明代码的正确性和识别运行时错误来提高 C/C++ 应用程序的可靠性。Polyspace 软件使用先进的验证技术对您的源代码进行全面彻底的验证。
由于 Polyspace 软件会验证代码的所有执行情况,因此它可以识别:
从不出错的代码
总是出错的代码
不可达代码
可能出错的代码
借助这些信息,您可以了解有多少代码不包含运行时错误,并可以通过修复错误来提高代码的可靠性。
您还可以通过使用 Polyspace 验证软件来检查您的代码是否符合既定的编码标准(例如 MISRA C™、MISRA™ C++ 或 JSF® C++ 标准),从而提高代码质量。1
缩短开发时间
Polyspace 软件通过自动执行验证过程并帮助您有效地审查验证结果来缩短开发时间。您可以在开发过程中随时使用该软件。但是,在编码的早期阶段使用该软件可以尽早发现错误,降低修复错误的成本。
您可以使用 Polyspace 软件在编译前验证源代码。要验证源代码,您需要在工程中设置验证参数、运行验证并审查结果。与使用手动方法或使用需要修改代码或运行测试用例的工具相比,此过程花费的时间要少得多。
对结果进行着色可帮助您快速识别错误。您在调试上花费的时间会更少,因为您可以看到错误在源代码中的确切位置。修复错误后,您可以轻松地再次运行验证。
Polyspace 验证软件可帮助您有效利用时间。由于了解代码中未出错的部分,您可以专注于已证实(红色代码)或潜在错误(橙色代码)的代码。
审查可能出错的代码(橙色代码)可能很耗时,但 Polyspace 软件可以帮助您完成审查过程。您可以使用过滤器来重点查看某些类型的错误,也可以让软件标识您应该审查的代码。
改进开发流程
Polyspace 软件可简化验证参数和结果的共享,使开发团队能够共同努力提高产品的可靠性。设置验证参数后,开发人员可以在同一应用程序的其他文件中重复使用这些参数。
Polyspace 验证软件支持贯穿整个开发流程的代码验证:
单个开发人员可以在初始编码阶段发现并修复运行时错误。
质量保证工程师可以检查应用程序的整体可靠性。
管理人员可以基于验证结果生成报告,监控应用程序的可靠性。
另请参阅
主题
1 MISRA and MISRA C are registered trademarks of MISRA Ltd., held on behalf of the MISRA Consortium.