关于Polyspace的静态分析的详细解析和应用

Polyspace是MathWorks产品家族的一员, 也许有人还不知道它能做什么以及作用原理是什么。简单来说，Polyspace是基于抽象解释原理的代码级静态分析和验证工具。

的确，由于时间和成本的关系我们不可能做穷举测试，但并不能就此推断我们没有测试的工况是安全的。

以汽车行业为例，已发生的多次召回事件经分析是因为软件缺陷尤其是运行时错误（run-time error）造成的。所谓的运行时错误，是指在通常的调试过程中需要程序运行起来之后才可能显现的错误，如指针越界、数据溢出等。换句话说，如果测试用例没有覆盖到特定的输入条件时，这些问题可能就没有机会被发现。

Windows平台下调试运行时错误发生的案例

除汽车行业以外，航空航天、铁路、医疗等所谓高完整性系统行业，嵌入式软件往往承载着系统大部分重要功能的实现，一旦发生问题会带来异常严重的后果。软件的静态分析作为动态功能测试的重要补充，在这些行业应用非常广泛。

所谓的静态分析，指在不运行程序的情况下，基于数学方法的分析来验证代码是否满足规范性、安全性、可靠性、可维护性等指标的一种代码分析技术。通俗地说，静态分析可以通过不写测试用例达到动态穷举测试的效果，是用来提高代码鲁棒性和证明软件安全性的重要手段。

Polyspace所采用的静态分析方法是抽象解释，是软件形式化验证方法(Formal Verification)的一种，它在处理复杂的计算问题或模型的过程中通过对问题进行近似抽象，取出其中的关键部分进行分析，从而减少问题的复杂程度。

抽象解释

简单举例，判断x/(x-y)是否有除零的风险的问题可以转换为左下图 x和y的取值范围是否有可能落在y=x的红线上。Polyspace基于程序控制结构、函数调用关系、多任务分析等，通过复杂的数据流析取过程抽象到右下图绿色多面空间中来判断是否有可能落在y=x上。

Polyspace中的抽象解释

经Polyspace分析后的代码结果以不同颜色表:

绿色代表为安全代码，无需花过多精力审查；

红色代码问题代码，需要立刻解决；

灰色代表不可达代码，需要审查是设计错误还是有意为之；

橙色代表有风险代码，需要重点审查。

另外还可以设定编码规范(如MISRA)和自定义代码风格，违反之处以紫色显示；同时可以看到代码变量随控制流的数据范围变化情况，快速查找和定位问题原因。

Polyspace的分析结果

不论是自动代码还是手写代码甚或混合代码，Polyspace可以承担类似“质量门”的角色，帮助查找常见软件缺陷、进行代码规范检查、提供软件度量信息，更进一步通过证明不存在运行时错误交付安全代码，大大提高代码审查的效率并可提供安全认证所需的相关证据。