破解嵌入式软件质量难题: 消除缺陷证明无运行时错误

概述

在嵌入式系统软件开发与测试过程中：写代码严重依赖于工程师的经验，容易引入错误（比如，比较等号与赋值等号编码失误，内存忘记释放…，多任务资源访问加锁顺序不一致，这些问题一旦出现会耗费大量资源去定位）；防御式编程，造成冗余，影响代码效率，需要增加额外测试用例用于满足覆盖率需求；基于需求的单元测试/集成测试/系统测试，能保证基本功能的正确性，但有限的测试用例始终无法做到对代码的完全充分测试，一旦出现问题（比如：并发访问导致的数据竞争，死锁），难以复现，定位，更不要说修复。人工评审效率低下，人工评审同样依赖于评审人经验；那是否有一套行之有效的方法来改善上述问题了，答案是在编码阶段以及功能测试开始之前引入静态分析技术作为对开发人员经验以及功能测试用例的补充，早期发现问题，修复问题，提升人工评审效率从而降低项目成本加速量产。

亮点包括

• 静态分析的误报与漏报与基于抽象解释的形式化验证方法
• 确切发现问题并精准定位根源
• 可疑情况分析
• 证明软件没有运行时错误
• 安全认证的支持和证物的生成
• 利用并行计算加速代码分析

关于演示者

胡乐华，MathWorks中国高级应用工程师，专注于基于模型设计在航空航天产品的设计开发的应用，有多年MathWorks高级培训经验。加入MathWorks之前，曾就职于霍尼韦尔中国和中航工业，分别从事机载软件开发和直升机飞行系统仿真。胡乐华毕业于沈阳航空航天大学，拥有理学学士和工学硕士学位。