Presentation Title By Author 2014 The MathWorks, Inc. 1
使用 Polyspace 进行软件代码运行错误检查和验证 李春彦 应用工程师 MathWorks China 2014 The MathWorks, Inc. 2
内容 Polyspace 背景介绍 Polyspace 产品功能及使用技巧 在基于模型设计开发流程中使用 Polyspace Polyspace 及相关工具对认证的支持 3
Hello, Polyspace! 1996 Alain Deutsch 时任 INRIA( 法国国家信息与自动化研 究所 ) 研究员 ; 成功地将抽象解释方法用于 Ariane 5 Ada 代码的检 查 ; 1999 成立了 2007 Daniel Pilaud Alain Deutsch 收购 Polyspace 4
Polyspace: 静态代码分析工具 作用 : 解决软件的鲁棒性问题, 确保软件的安全性和可靠性 ; 能够做什么? 发现编码错误 检查编码规则一致性 (MISRA/JSF) 提供代码静态度量信息 ( 圈复杂度等 ) 证明代码中确定存在或者确定不存在的错误 表示代码已经达到了预期的质量水平 认证帮助 :DO-178 C, ISO 26262, 5
嵌入式系统的缺陷 与需求不一致 时间相关的错误 Simulink Design Verifier 仿真, 集中测试, 实验测试 HIL 测试 静态错误 编译器, 静态分析工具, 人工代码评审, 建模规则检查 Polyspace 缺陷 什么样的工具和流程能够发现这些缺陷? 你能证明系统不存在特定缺陷吗? 运行时错误 Polyspace 6
常见的软件代码错误 运行时错误 40% 左右的软件错误为运行时错误 ; 运行时错误是软件代码的潜在缺陷, 并不频繁出现 ; 运行期错误会导致系统崩溃和意外的行为 并发问题 编程错误 不可达代码 静态或者动态内存错误 7
Polyspace C / C ++ 产品系列 Polyspace Bug Finder 快速找到嵌入式软件中的错误 检查代码符合 MISRA 和 JSF 编码规则 供软件工程师日常使用 Polyspace Code Prover 证明代码是安全和可靠的 ( 是否包含运行时错误 ) 软件组件的深层验证 执行 QA 对生产就绪代码的签收 还支持 Ada 语言代码证明 8
使用 Polyspace 迎接复杂系统设计的挑战 现代汽车动力系统 500-1,000(KLOC) 减少软件故障风险 波音 787 飞控系统 6,500 (KLOC) 航天器 * 3-1,700 (KLOC) 应用于质量关键 业务关键或者高完整性系统中 ; 减少产品代码中可能导致系统崩溃的潜在错误 缩短软件测试和验证周期 减少软件的鲁棒性测试 ; 显著缩短系统开发周期 *Automated Software Verification & Validation: An emerging approach for ground operations Bell and Brat, NASA 9
内容 Polyspace 背景介绍 Polyspace 产品功能及使用技巧 在基于模型设计开发流程中使用 Polyspace Polyspace 及相关工具对认证的支持 10
如何找到代码的运行时错误? 0 k=ioread_i32(); 1 I=2; 2 J=K+5; 3 while (I<10) { 4 I=I+1; 5 J=J+3; 6 } 7 8 /(I-J); 当 k=-19 时, 第 8 行会出现除零错误 第 8 行有没有潜在的 除零 风险? 11
Polyspace 是如何显示的? 0 k=ioread_i32(); 1 I=2; 2 J=K+5; 3 while (I<10) { Polyspace 4 I=I+1; 5 J=J+3; 6 } 7 8 /(I-J); 12
Polyspace 的结果 A colorful world P r o v e n Green: reliable safe pointer access Red: faulty out of bounds error Gray: dead unreachable code Orange: unproven may be unsafe for some conditions static void pointer_arithmetic (void) { int array[100]; int *p = array; int i; for (i = 0; i < 100; i++) { *p = 0; } p++; variable I (int32): [0.. 99] assignment of I (int32): [1.. 100] if (get_bus_status() > 0) { if (get_oil_pressure() > 0) { *p = 5; } else { i++; } } i = get_bus_status(); Purple: violation MISRA-C/C++ or JSF++ code rules Range data tool tip } if (i >= 0) { *(p - i) = 10; } 13
Polyspace 行业应用 Polyspace 对于任何类型的代码都是高效的 不同应用的代码缺陷分布 不同应用的代码证明比例 98% 意味着只有 2% 的检查是橙色的 Polyspace 采用的形式化方法是通用的 14
Polyspace 产品的功能 第三方 IDE 环境的集成 Visual Studio,Eclipse 能够与用户的构建环境进行集成并自动生成 Polyspace 配置文件 polyspace-configure 自动代码生成工具的集成 Embedded Coder, Target Link, IBM Rational Rhapsody 支持在集群上进行部署安装 利用集群优势加快 Polyspace Code Prover 的验证速度 15
Polyspace 支持与第三方 IDE 环境集成 支持的环境有 Eclipse,Visual Studio 16
Polyspace 配置工具 :polyspace-configure 与用户的构建环境进行集成, 自动生成 Polyspace 工程或配置文件 命令 :polyspace-configure 使用方法 : R2014a Video 17
Polyspace 支持与自动代码生成工具进行集成 Embedded Coder, TargetLink, IBM Rational Rhapsody 18
内容 Polyspace 背景介绍 Polyspace 产品功能及使用技巧 在基于模型设计开发流程中使用 Polyspace Polyspace 及相关工具对认证的支持 19
在开发流程中引入 Polyspace 需求 验证 外部软件组件 结构设计 集成测试 单元设计 单元测试 实现 20
在开发流程中引入 Polyspace 需求 验证 外部软件组件 结构设计 集成测试 单元设计 使用 Polyspace Bug Finder: 消除编码错误 检查编码规则 (i.e. MISRA) 单元测试 实现 21
在开发流程中引入 Polyspace 需求 验证 外部软件组件 结构设计 使用 Polyspace Code Prover: 证明代码不存在运行期错误 证明单元符合设计要求 ( 输入 / 输出 ) 集成测试 单元设计 单元测试 实现 22
在开发流程中引入 Polyspace 需求 结构设计 使用 Polyspace Bug Finder: 获取代码质量度量信息 编码规则检查 发现代码集成缺陷 使用 Polyspace Code Prover: 证明单元之间不存在运行期错误 证明符合设计要求 ( 输入 / 输出 ) 证明共享内存的安全性 验证 外部软件组件 集成测试 单元设计 单元测试 实现 23
在开发流程中引入 Polyspace 需求 发布 Polyspace 结果 Polyspace Web Metrics 生成报告 验证 外部软件组件 结构设计 集成测试 单元设计 单元测试 实现 24
内容 Polyspace 背景介绍 Polyspace 产品功能及使用技巧 在基于模型设计开发流程中使用 Polyspace Polyspace 及相关工具对认证的支持 25
软件质量目标 (Software Quality Objectives) 在 Polyspace 中设定软件质量目标 确定文件 模块或者组件是否达到了预定质量目标 定义软件质量目标门槛 软件代码度量信息 违反编码规则数量 红色 灰色 橙色的检查数量 将 SQO 作为流程指南 根据质量目标来指定工具使用和流程改进的计划 26
使用 Polyspace 进行 DO-178 认证 MathWorks can provide a DO-178 Qualification Kit to help qualify Polyspace for your DO-178 certification projects 使用 DO Qualification Kit, 您可以 证明 Polyspace 产品可以用于满足 DO-178C 和相关标准如 DO-330 产品开发活动 帮助获得认证 套件包括 : 文档, 测试用例和流程指导书 工具资质证明计划, 工具的使用要求和其它材料 允许针对特定项目对工具认证套件进行修改 Polyspace Bug Finder is a Criteria 3 Tool for DO-178C Polyspace Code Prover is a Criteria 2 Tool for DO-178C 27
Polyspace 支持 DO-178B/C 认证 代码与软件设计结构一致 (architecture) 数据字典, 函数调用树 代码是可以被验证的 (Verifiable) 发现不可达代码 代码要符合编码规则 MISRA C, MISRA C++, 或 JSF++ 规则检查 静态度量信息, 例如圈复杂度 ( 编码标准的一部分 ) 代码是准确的 (Accurate) 和一致的 (Consistent) 发现代码中的运行期错误, 例如除零 溢出 变量未初始化等 28
使用 Polyspace for IEC 61508, ISO 26262, EN 50128, IEC 62304 认证 MathWorks can provide a Certification Kit for IEC 61508 related standards 使用认证套件, 您可以 在推荐流程下使用 Polyspace 来验证您的代码 帮助获得认证 套件包括 工具资质证书, 审核材料和测试套件 可以使用 Polyspace 的工具证明材料 推荐的工作流程 29
Polyspace 可以提供的帮助 1 编码 / 代码评审 避免编程错误和高效的代码评审 开发 过程 2 单元测试 / 集成测试 有效减少健壮性测试 3 认证 / 文档化 认证支持 / 自动生成报告 31