维基百科

Polyspace

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

Polyspace
开发者MathWorks [1]
当前版本R2020b（2020年9月15日，​4年前​（2020-09-15））
操作系统跨平台[2]
类型静态程序分析
许可协议专有软件
网站https://mathworks.com/products/polyspace.html

常见用法

编辑

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的工具得到分析的结果。

相关条目

编辑

参考资料

编辑
  1. ^ Pele, Anne-Francoise. The Mathworks acquires PolySpace Technologies. EETimes. 2007-04-25 [2010-08-13]. （原始内容存档于2012-02-11）. 
  2. ^ The MathWorks - Polyspace - Requirements
  3. ^ Deutsch, Alain. Static Verification of Dynamic Properties (PDF). Polyspace Technologies. 27 November 2003 [2014-05-17]. （原始内容 (PDF)存档于2012-03-13）. 
  4. ^ Brat, Guillaume. Experimental Evaluation of Verification and Validation Tools on Martian Rover Software. Formal Methods in System Design. 2004 [2010-08-13]. [永久失效链接]
  5. ^ 5.0 5.1 Exponent. Exponent's Investigation of Toyota ETCS-i Vehicle Hardware and Software. Exponent. 2012-09-24 [2010-09-07]. （原始内容存档于2014-07-27）. 
  6. ^ MathWorks: static code analysis （页面存档备份，存于互联网档案馆）.
  7. ^ Software Metrics-MATLAB. India: MathWorks. [2015-08-27]. （原始内容存档于2016-04-02）. 
  8. ^ Jones, Paul; Jetley, Raoul; Abraham, Jay. A Formal Methods-based verification approach to medical device software analysis. Embedded Systems Design. 2010-02-09 [2010-08-16]. （原始内容存档于2014-07-25）. 
  9. ^ Wissing, Klaus. Static Analysis of Dynamic Properties - Automatic Program Verification to Prove the Absence of Dynamic Runtime Errors (PDF). Workshop on Applied Program Analysis. 2007-09-27 [2010-08-13]. （原始内容存档 (PDF)于2011-07-18）. 

外部链接

编辑
检索自“https://zh.wikipedia.org/w/index.php?title=Polyspace&oldid=79065679”