Polyspace静态程序分析的工具,利用抽象释义的方式进行大规模的分析,可以侦测C语言、C++或是Ada程式的原始码中,是否有特定类型的执行期错误,或是证明没有这类的错误。此工具也可以检查原始码是否符合特定的代码标准(如MISRA C/C++, SEI CERT C/C++(CWE), JSF AV C++, AUTOSAR C++)[3]

常见用法

Polyspace可以检查原始码,确认是否有潜在的执行期错误RTE(Run Time Error),像是算术溢出缓冲区溢出除以零、矩阵index溢位以及其他可能发生的错误。软体开发者以及品质保证主管可以利用这些资讯(颜色)来识别程式中哪些部份可能有错(橘色)、绝对有问题(红色)、绝对没问题(绿色)、无法执行dead code(灰色),并依其严重程式来选择哪些要优先处理。程式码的其他部份会标示为尚未证明的部份,可以再个别进行代码评审[4][5]

Polyspace亦可检查Coding Standard,如MISRA C/C++、SEI CERT C/C++、AUTOSAR C++之类的程式码标准及指南会试著提升程式的品质、可携性及可靠度。Polyspace会确认C及C++的原始码是否符合这些程式码标准中的特定一部份规则[6]

另外Polyspace亦可进行Code Metrics的量测,如注解密度(Comment density)、循环复杂度(Cyclonmatic Complexity)等

其他功能

Polyspace产品系列也包括了Polyspace Bug Finder及Polyspace Code Prover。工具的设计上Code Prover是基于Bug Finder上来叠加功能的,亦即Code Prover包含Bug Finder的功能。

  • Polyspace基于IEC61508-3/ISO26262-8已获得Tüv Süd的认证。Polyspace的分析可用于涵盖IEC61508/ISO26262标准part 6“软体产品开发”的一系列指南。 Polyspace的客户端/服务器架构简化并简化了管理符合编码标准(例如MISRA)的过程,这是IEC61508/ISO 26262要求中静态分析方面的一个关键特征。
  • Polyspace Bug Finder 利用原始码的静态程序分析找出程式中的软体错误(Bug Detection),可以找到数值计算、程式、记忆体等不同方面的错误。Bug Finder也会产生软体度量(Code Metrics),例如原始码中的注解密度、循环复杂度、代码行数、参数、函式的呼叫层级、程式中已找到的软体错误等[7]
  • Polyspace Code Prover 会将原始码用颜色编码方案标示(红色:会产生RTE、绿色:不会产生RTE、橘色:可能产生RTE、灰色:Dead code程式码不会执行),表示原始码中不同元素的状态[8]。Code Prover会使用形式化方法(Formal Verification)为基础的静态代码分析来验证程式语言层级的程式执行情形[5]。Code Prover会考虑程式中各变数的可能的值,在每一行程式提供正常及不正常使用情形下的诊断结果[9]
  • Polyspace 亦提供Client/Server的功能,可以利用Client端定义work item然后submit工作到Server端去执行。另外可以透过Access的工具得到分析的结果。

相关条目

参考资料

外部链接

Wikiwand in your browser!

Seamless Wikipedia browsing. On steroids.

Every time you click a link to Wikipedia, Wiktionary or Wikiquote in your browser's search results, it will show the modern Wikiwand interface.

Wikiwand extension is a five stars, simple, with minimum permission required to keep your browsing private, safe and transparent.