目标:通过一个实例来熟悉Polyspace 软件。

• Polyspace 软件概述
• 简单的的代码验证示例
• 使用Polyspace Server™远程验证

目标:验证也许不能满足ANSI C 标准的代码，考虑运行环境。

• 常见的运行环境设置
• 处理特定处理器要求的代码
• 定义执行内容
• 设置目标硬件信息

目标:验证也许不能满足标准Ada语言标准的代码，考虑运行环境。

• 常见的运行环境设置
• 处理特定处理器要求的代码
• 定义执行内容
• 设置目标硬件信息

目标: 熟练解释 Polyspace 结果。

• 抽象解释技术
• 调用树分析
• 原代码导航
• 执行顺序
• 变量范围
• 全局变量

目标: 学习Polyspace如何在验证过程中处理缺失代码，如何得到更有意义的验证结果。

• 鲁棒性验证和上下文验证
• 函数打桩
• 数据范围设置

目标: 学习Polyspace如何在验证过程中处理缺失代码，如何得到更有意义的验证结果。

• 鲁棒性验证和上下文验证
• 函数打桩
• 数据范围设置

目标:使用Polyspace中的诊断工具发现运行时错误。

• C代码检查概述
• 源代码中的检查标记位置
• 检查描述
• 相关验证选项

目标: 使用Polyspace中的诊断工具发现运行时错误。

• C代码检查概述
• 源代码中的检查标记位置
• 检查描述
• 相关验证选项

目标:处理包含大范围无法验证(橙色)代码的结果。

• 定义验证难度
• 执行快速检查 (PI控制器例子)
• 执行选择性橙色检查 (PI控制器例子)
• 设置验证精度
• 使用自动橙色测试器
• 优先处理橙色检查
• 复核橙色检查
• 使用帮助模式

目标: 使用PolySpace Launcher 检测代码是否遵从MISRA C® 规则。

• MISRA C 编码规则概述
• 运行MISRA C 检测
• 检查MISRA C 验证结果
• MISRA C 标准对PolySpace验证结果的影响

目标:使用网络度量和报告对验证结果进行共享和分类，生成标准报告。

• 共享结果
• 使用网络度量
• 测试软件质量目标
• 创建文档

目标:回顾验证大规模代码时有用的步骤和选项。

• 设置上下文验证
• 改善上下文验证的结果
• 比较鲁棒性验证和上下文验证