Polyspace

Polyspace靜態程序分析的工具,利用抽象释义的方式進行大規模的分析,可以偵測C語言、C++或是Ada程式的原始碼中,是否有特定類型的執行期錯誤,或是證明沒有這類的錯誤。此工具也可以檢查原始碼是否符合特定的代碼標準(如MISRA C/C++, SEI CERT C++, JSF AV C++, AUTOSAR C++)[3]

Polyspace
開發者MathWorks [1]
穩定版本
R2020b
(2020年9月15日2020-09-15
操作系统跨平台[2]
类型靜態程序分析
许可协议专有软件
网站https://mathworks.com/products/polyspace.html

常見用法

Polyspace可以檢查原始碼,確認是否有潛在的執行期錯誤RTE(Run Time Error),像是算術溢出缓冲区溢出除以零、矩陣index溢位以及其他可能發生的錯誤。軟體開發者以及品質保證主管可以用這些資訊來識別程式中某一部份可能有錯,或者證實是可靠的。程式碼的其他部份會標示為尚未證明的部份,可以再個別進行代碼評審[4][5]

MISRA C之類的程式碼標準及指南會試著提昇程式的品質、可攜性及可靠度。Polyspace會確認C及C++的原始碼是否符合這些程式碼標準中的特定一部份規則[6]

其他功能

Polyspace產品系列也包括了Polyspace Bug Finder及Polyspace Code Prover。工具的設計上Code Prover是基於Bug Finder上來疊加功能的,亦即Code Prover包含Bug Finder的功能。

  • 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. . EETimes. 2007-04-25 [2010-08-13]. (原始内容存档于2012-02-11).
  2. The MathWorks - Polyspace - Requirements
  3. Deutsch, Alain. (PDF). Polyspace Technologies. 27 November 2003 [2014-05-17]. (原始内容 (PDF)存档于2012-03-13).
  4. Brat, Guillaume. . Formal Methods in System Design. 2004 [2010-08-13].
  5. Exponent. . Exponent. 2012-09-24 [2010-09-07]. (原始内容存档于2014-07-27).
  6. MathWorks: static code analysis 页面存档备份,存于.
  7. . India: MathWorks. [2015-08-27]. (原始内容存档于2016-04-02).
  8. Jones, Paul; Jetley, Raoul; Abraham, Jay. . Embedded Systems Design. 2010-02-09 [2010-08-16]. (原始内容存档于2014-07-25).
  9. Wissing, Klaus. (PDF). Workshop on Applied Program Analysis. 2007-09-27 [2010-08-13]. (原始内容存档 (PDF)于2011-07-18).

外部連結

This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.