使用静态分析加速软件开发和验证流程

为了祖国的未来，快来关注我们吧

作者简介

龚小平，MathWorks公司中国区高级应用工程师，主要负责基于模型的设计和从模型到代码的测试验证在汽车及其他工业领域中的应用，具有10年以上的MATLAB/Simulink使用经验。加入MathWorks之前，曾从事汽车电控系统的设计开发，在系统工程和软件工程方面有丰富的经验。

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

试想在软件交付之前，质量工程师(Q)和开发工程师（D）有如下对话：

>>>要交付的软件经过充分测试了吗?

当然，我已经跑完所有的测试用例了。

>>>测试用例是否包含所有的可能性？

呃，没有,我不可能做穷举测试啊。

的确，由于时间和成本的关系我们不可能做穷举测试，但并不能就此推断我们没有测试的工况是安全的。以汽车行业为例，已发生的多次召回事件经分析是因为软件缺陷尤其是运行时错误（run-timeerror）造成的。所谓的运行时错误，是指在通常的调试过程中需要程序运行起来之后才可能显现的错误，如指针越界、数据溢出等。换句话说，如果测试用例没有覆盖到特定的输入条件时，这些问题可能就没有机会被发现。

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

除汽车行业以外，航空航天、铁路、医疗等所谓高完整性系统行业，嵌入式软件往往承载着系统大部分重要功能的实现，一旦发生问题会带来异常严重的后果。软件的静态分析作为动态功能测试的重要补充，在这些行业应用非常广泛。所谓的静态分析，指在不运行程序的情况下，基于数学方法的分析来验证代码是否满足规范性、安全性、可靠性、可维护性等指标的一种代码分析技术。通俗地说，静态分析可以通过不写测试用例达到动态穷举测试的效果，是用来提高代码鲁棒性和证明软件安全性的重要手段。

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

抽象解释

（图片来源于SoonhoKong的CMU15-414BugCatching:AutomatedProgramVerificationandTesting-AbstractInterpretation）

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

Polyspace中的抽象解释

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

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

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

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

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

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

Polyspace的分析结果

Polyspace根据不同的静态分析深度分为BugFinder和CodeProver两个产品。

BugFinder-快速分析，用于查找常见软件缺陷，

CodeProver-深度分析，用于证明软件不存在特定的运行时错误。

此外，两者都具有编码规范检查和软件质量度量功能。下图展示了BugFinder和CodeProver分析所得结果中不同颜色检查所代表的含义：

鉴于BugFinder和CodeProver不同特点，将其合理应用到软件开发和验证流程中能得到事半功倍的效果。以下将说明在V开发模式中Polyspace的应用场景案例：

软件实现阶段

软件实现即编码阶段，在该阶段软件工程师希望随着编码进程查找并修复软件缺陷和违背编码规范之处，BugFinder可以助其快速迭代分析。值得一提的是，随着嵌入式应用与外界交互的逐渐增加，网络安全问题越来越突出，如数据来源的可靠性问题等。BugFinder支持了当前主流的网络安全标准检查，如CWE、CERT、ISO-17961等。编码规范检查支持C代码的MISRA2004和2012等标准，C++代码支持MISRAC++和JSFC++等标准，代码风格和命名规范则提供了简单易行的定制界面和方法。

单元测试阶段

软件单元在交付之前不仅需要满足功能需求（功能性），也需要证明安全合格（鲁棒性）。前者可以采用运行基于需求的测试用例，比较测试结果和期望值实现；后者则可以借助于CodeProver强大的深度分析能力，修复错误代码，审查可疑代码，最终交付已证明安全的可信代码。通常鲁棒性分析可以安排在功能性测试之前，以提升单元测试的效率。

集成测试阶段

在软件单元合格交付之后，集成阶段需要将大量源代码文件进行集成并测试，在集成功能测试之前，同样建议先使用BugFinder查找并排除常见的软件集成问题，如声明的不匹配、共享变量的数据冲突等。

验收测试阶段

验收测试阶段，在软件正式交付或发布之前，使用CodeProver进行应用级的安全性证明，并获取相应的软件度量信息(如圈复杂度)等，与行业或企业的软件质量目标（SQO）进行比较，确认是否符合交付标准，并提交可自动生成的质量报告。

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

长按识别二维码，免费下载《嵌入式软件开发使用静态分析的十大优势》电子书。