PDF《Presentation Title》

1 ?

2014 The MathWorks, Inc.

Presentation Title By Author

2 ?

2014 The MathWorks, Inc. 使用Polyspace进行软件代码运行错误检 查和验证 李春彦 应用工程师 MathWorks China

3 内容 ? Polyspace背景介绍 ? Polyspace产品功能及使用技巧 ? 在基于模型设计开发流程中使用Polyspace ? Polyspace及相关工具对认证的支持

4 1996 Alain Deutsch时任INRIA(法国国家信息与自动化研 究所)研究员;

成功地将抽象解释方法用于Ariane

5 Ada代码的检 查;

1999 成立了

2007 收购Polyspace Hello, Polyspace! Daniel Pilaud Alain Deutsch

5 Polyspace:静态代码分析工具 ? 作用:解决软件的鲁棒性问题,确保软件的安全性 和可靠性;

? 能够做什么? C 发现编码错误 C 检查编码规则一致性(MISRA/JSF) C 提供代码静态度量信息(圈复杂度等) C 证明代码中确定存在或者确定不存在的错误 C 表示代码已经达到了预期的质量水平 C 认证帮助:DO-178 C, ISO 26262, …

6 嵌入式系统的缺陷 静态错误 与需求不一致 时间相关 的错误 运行时 错误 编译器, 静态分析工具, 人工代码评审, 建模规则检查 仿真, 集中测试, 实验测试 什么样的工具和流程能够发现这些缺陷? 你能证明系统不存在特定缺陷吗? 缺陷 Simulink Design Verifier Polyspace HIL测试 Polyspace

7 常见的软件代码错误 ? 运行时错误 C 40%左右的软件错误为运行时错误;

C 运行时错误是软件代码的潜在缺陷,并不频繁出现;

C 运行期错误会导致系统崩溃和意外的行为. ? 并发问题 ? 编程错误 ? 不可达代码 ? 静态或者动态内存错误

8 Polyspace C / C ++产品系列 ? Polyspace Bug Finder C 快速找到嵌入式软件中的错误 C 检查代码符合MISRA和JSF编码规则 C 供软件工程师日常使用 ? Polyspace Code Prover C 证明代码是安全和可靠的(是否包含运行时错误) C 软件组件的深层验证 C 执行QA对生产就绪代码的签收 还支持Ada语言代码证明

9 使用Polyspace迎接复杂系统设计的挑战 ? 减少软件故障风险 C 应用于质量关键、业务关键或者高完整性系统中;

C 减少产品代码中可能导致系统崩溃的潜在错误. ? 缩短软件测试和验证周期 C 减少软件的鲁棒性测试;

C 显著缩短系统开发周期. *Automated Software Verification &

Validation: An emerging approach for ground operations Bell and Brat, NASA 现代汽车动力系统 500-1,000(KLOC) 波音787飞控系统 6,500 (KLOC) 航天器* 3-1,700 (KLOC)

10 内容 ? Polyspace背景介绍 ? Polyspace产品功能及使用技巧 ? 在基于模型设计开发流程中使用Polyspace ? Polyspace及相关工具对认证的支持

11 0 k=ioread_i32();

1 I=2;

2 J=K+5;

3 while (I 0) { *p = 5;

} else { i++;

} } i = get_bus_status();

if (i >

= 0) { *(p - i) = 10;

} } Polyspace的结果 Green: reliable safe pointer access Red: faulty out of bounds error Gray: dead unreachable code Orange: unproven may be unsafe for some conditions variable '

I'

(int32): [0 .. 99] assignment of '

I'

(int32): [1 .. 100] Range data tool tip Purple: violation MISRA-C/C++ or JSF++ code rules A colorful world P r o v e n

14 Polyspace行业应用 ? Polyspace对于任何类型的代码都是高效的 Polyspace采用的形式化方法是通用的 不同应用的代码缺陷分布 不同应用的代码证明比例 98%意味着只有2%的检查是橙色的

15 Polyspace产品的功能 ? 第三方IDE环境的集成 C Visual Studio,Eclipse ? 能够与用户的构建环境进行集成并自动生成Polyspace配 置文件 C polyspace-configure ? 自动代码生成工具的集成 C Embedded Coder, Target Link, IBM Rational Rhapsody ? 支持在集群上进行部署安装 C 利用集群优势加快Polyspace Code Prover的验证速度