你的代码敢上Polyspace跑吗?

嵌入式代码动态验证

在嵌入式开发中,代码静态分析工具相信大家应该都熟悉,都用过像PClint,understand C等,但对于动态验证,运行时错误验证工具还是不多,今天给大家介绍一款代码运行错误动态验证工具---Polyspace,本人有幸使用过这款优秀的软件,绝对不是广告噢呵呵,有兴趣的猿友可以到mathwork官网下载使用版,对你的代码进行验证,让你的代码更安全,更规范。Polyspace 目前已经被Mathwork 纳入麾下,称为mathwrok旗下的产品,如果各位以前用过matlab的话应该对mathwrok公司不陌生,Polyspace 分为Polyspace Code Prover 与 Polyspace Bug Finder两部分,可以结合使用。可以到mathwork官网搜索Polyspace下载试用版如下图所示:

Polyspace Code Prover™ 可以证明 C 和 C++ 源代码中不存在溢出、被零除、数组访问超出边界以及其他某些运行时错误。整个过程无需执行程序、植入代码,也不需要测试用例。Polyspace Code Prover 使用静态分析和基于形式化方法的抽象释义。该程序可以用于手写代码、生成的代码或二者的混合。每项操作均采用颜色标记,分别表示代码无运行时错误、已证明失效、无法达到或未经证明。 Polyspace Code Prover 还会显示变量和函数返回值的范围信息,并可以证明变量是否超出指定范围限制。这些结果可以发布到控制面板上,以跟踪质量指标并确保符合软件质量目标。Polyspace Code Prover 可以集成到构建系统中以执行自动验证。

  • 主要特性
  • 验证 C 和 C++ 嵌入式软件
  • 检测运行时错误
  • 查看范围信息
  • 跟踪软件质量指标
  • 依据代码验证结果回溯至 Simulink 模型
  • 实现代码验证流程自动化
  • 创建认证工件

检测运行时错误 Polyspace Code Prover 将抽象释义与静态代码分析结合使用,以识别和诊断溢出、被零除和指针越界等运行时错误。这项技术可以完整而全面验证所有运行时情况,并为每项代码自动提供诊断报告,包括已证明、已失败、无法达到或未经证明诊断。在 Polyspace Code Prover 生成的验证结果中,每一项 C 或 C++ 运算均采用颜色编码表示其状态: 绿色: 已证明没有运行时错误 红色:已证明在每次运行时都有错误 灰色:已证明无法达到(可能表示存在功能性问题) 橙色:未经证明,在某些情况下可能有错

跟踪软件质量指标 您可以定义一个集中式的质量模型,来跟踪运行时错误、代码复杂度和编码违规。使用这些指标,可以在代码从首次迭代到最终交付的完善过程中,持续跟踪预定义的软件质量目标。通过衡量代码质量改进率,Polyspace Code Prover 使开发人员、测试人员和项目经理能够致力于编写和交付高质量的代码。

实现代码验证流程自动化 通过将 Polyspace 整合到构建流程中,您可以将 Polyspace Code Prover 作为持续集成流程的一部分。您可以自动调度验证作业并设置电子邮件通知。您可以配置Polyspace Code Prover 将验证作业发布到集群计算机(使用 MATLAB Distributed Computing Server),并发送电子邮件通知结果。结果包含与上一版本代码的差异。这些差异由服务器自动计算。 您可以定义分析的频率、定义质量模型,指定需要分析的代码部分,以及接收结果的用户电子邮件地址。此外,您还可以定义自动验证需要涵盖构建过程的哪些特性。 Polyspace 可以生成各种格式的文档,如PDF, wrod,Html等等,方便归档汇报。还可以远程访问。最终生成的报告和结果 会显示代码的最终质量、高亮显示已审查的部分、生成代码指标、记录所使用的编码规则以及运行时错误状态。您可以将报告发布为 PDF、HTML、RTF 以及其他格式。

嵌入式

程序猿

微信号:InterruptISR

原文发布于微信公众号 - 嵌入式程序猿(InterruptISR)

原文发表时间:2015-08-12

本文参与腾讯云自媒体分享计划,欢迎正在阅读的你也加入,一起分享。

发表于

我来说两句

0 条评论
登录 后参与评论

相关文章

来自专栏Golang语言社区

游戏系统设计

一、 服务器 1、逻辑与数据分离 2、读写分离 3、服务器分层 4、分区容错 HA a.路由服务器组 *1, 做到AB测试,添加功能开关,策略选择灰度测试发布。...

4237
来自专栏java一日一条

程序员编程的 7 + 1 条小贴士

用10分钟,20分钟甚至30分钟的时间来想想你需要什么,想想什么样的设计模式(如果有的话)适合你将要编码的东西。真的要好好想想,你会很庆幸“浪费”了那几分钟,当...

573
来自专栏Android干货园

Android 轻松实现百度地图定位

版权声明:本文为博主原创文章,转载请标明出处。 https://blog.csdn.net/lyhhj/article/details/49...

3961
来自专栏机器学习算法与Python学习

Torch7深度学习教程1

Torch7的本系列教程的主要目的是介绍Torch的入门使用。今天首先分享一下Torch7的安装。(在Ubuntu14.04安装torch7) 为什么选择Tor...

3026
来自专栏跨界架构师

分布式系统中的必备良药 —— RPC

  在上一篇分布式系统系列中《分布式系统中的必备良药 —— 服务治理》中阐述了服务治理的一些概念,那么与服务治理配套的必然会涉及到RPC框架。在当前互联网的大背...

2111
来自专栏睿哥杂货铺

Linux 性能诊断:快速检查单(Netflix版)

快速检查单(Quick Reference Handbook,QRH)是飞行员在飞行过程中依赖的重要指导性文件。

3837
来自专栏玉树芝兰

如何用R和API免费获取Web数据?

API是获得Web数据的重要途径之一。想不想了解如何用R调用API,提取和整理你需要的免费Web数据呢?本文一步步为你详尽展示操作流程。

1222
来自专栏非著名程序员

推荐几个适合新人上手的Python项目

962
来自专栏Python、Flask、Django

python内容识别

1545
来自专栏MessageQueue

译《Time, Clocks, and the Ordering of Events in a Distrib...》

《Time, Clocks, and the Ordering of Events in a Distributed System》大概是在分布式领域被引用的最...

982

扫码关注云+社区

领取腾讯云代金券