Polyspace
Polyspace是靜態程序分析的工具，利用抽象释义的方式進行大規模的分析，可以偵測C語言、C++或是Ada程式的原始碼中，是否有特定類型的執行期錯誤，或是證明沒有這類的錯誤。此工具也可以檢查原始碼是否符合特定的代碼標準（如MISRA C/C++, SEI CERT C/C++（CWE）, JSF AV C++, AUTOSAR C++）。
| 開發者 | MathWorks [1] |
|---|---|
| 当前版本 | R2020b（2020年9月15日） |
| 操作系统 | 跨平台[2] |
| 类型 | 靜態程序分析 |
| 许可协议 | 专有软件 |
| 网站 | https://mathworks.com/products/polyspace.html |
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的工具得到分析的結果。
相關條目
[编辑]參考資料
[编辑]- ^ Pele, Anne-Francoise. The Mathworks acquires PolySpace Technologies. EETimes. 2007-04-25 [2010-08-13]. （原始内容存档于2012-02-11）.
- ^ The MathWorks - Polyspace - Requirements
- ^ Deutsch, Alain. Static Verification of Dynamic Properties (PDF). Polyspace Technologies. 27 November 2003 [2014-05-17]. （原始内容 (PDF)存档于2012-03-13）.
- ^ Brat, Guillaume. Experimental Evaluation of Verification and Validation Tools on Martian Rover Software. Formal Methods in System Design. 2004 [2010-08-13].[永久失效連結]
- ^ 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）.
- ^ MathWorks: static code analysis （页面存档备份，存于互联网档案馆）.
- ^ Software Metrics-MATLAB. India: MathWorks. [2015-08-27]. （原始内容存档于2016-04-02）.
- ^ 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）.
- ^ 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）.
外部連結
[编辑]- Mathworks - Polyspace Static Analysis
- In memory of Alain Deutsch（页面存档备份，存于互联网档案馆） （PolySpace 技术的共同创造者）
- Software testing FAQ