imported>Wolfch 来自 2026年2月14日 (六) 15:18

2026-02-14T15:18:56Z

新页面

{{noteTA|G1=IT|1=zh-hant:執行期錯誤;zh-hans:运行时错误|2=zh-hant:可攜性;zh-hans:可移植性}}
{{Infobox Software
| name = Polyspace
| screenshot =
| caption =
| developer = [[迈斯沃克|MathWorks]] <ref>{{cite web | title=The Mathworks acquires PolySpace Technologies | last=Pele | first=Anne-Francoise | publisher=EETimes | date=2007-04-25 | url=http://www.eetimes.com/electronics-news/4187806/The-Mathworks-acquires-PolySpace-Technologies | accessdate=2010-08-13 | archive-date=2012-02-11 | archive-url=https://web.archive.org/web/20120211091351/http://www.eetimes.com/electronics-news/4187806/The-Mathworks-acquires-PolySpace-Technologies | dead-url=no }}</ref>
| latest_release_version = R2020b
| latest_release_date = {{Start date and age|2020|09|15}}
| operating_system = [[跨平台]]<ref>[http://www.mathworks.com/support/sysreq/current_release/polyspace/index.html?s_cid=wiki_polyspace_1 The MathWorks - Polyspace - Requirements]</ref>
| genre = [[靜態程序分析]]
| license = [[专有软件]]
| website = [https://mathworks.com/products/polyspace.html https://mathworks.com/products/polyspace.html]
| products = Polyspace Bug Finder, Polyspace Code Prover
}}

'''Polyspace'''是[[靜態程序分析]]的工具，利用[[抽象释义]]的方式進行大規模的分析，可以偵測C語言、C++或是Ada程式的[[原始碼]]中，是否有特定類型的[[執行期]]錯誤，或是證明沒有這類的錯誤。此工具也可以檢查原始碼是否符合特定的代碼標準（如[[MISRA C]]/C++, [[CERT程式撰寫標準|SEI CERT C/C++]]（CWE）, JSF AV C++, AUTOSAR C++）<ref>{{cite web | title=Static Verification of Dynamic Properties | last=Deutsch | first=Alain | publisher=Polyspace Technologies | date=27 November 2003 | url=http://nesl.ee.ucla.edu/courses/ee202a/2005f/papers/Static_Verification.pdf | accessdate=2014-05-17 | deadurl=yes | archiveurl=https://web.archive.org/web/20120313084616/http://nesl.ee.ucla.edu/courses/ee202a/2005f/papers/Static_Verification.pdf | archivedate=2012-03-13 }}</ref>。

== 常見用法 ==
Polyspace可以檢查原始碼，確認是否有潛在的執行期錯誤RTE（Run Time Error），像是[[算術溢出]]、[[缓冲区溢出]]、[[除以零]]、矩陣index溢位以及其他可能發生的錯誤。軟體開發者以及品質保證主管可以利用這些資訊（顏色）來識別程式中哪些部份可能有錯（橘色）、絕對有問題（紅色）、絕對沒問題（綠色）、無法執行dead code（灰色），並依其嚴重程式來選擇哪些要優先處理。程式碼的其他部份會標示為尚未證明的部份，可以再個別進行[[代碼評審]]<ref>{{cite web | title=Experimental Evaluation of Verification and Validation Tools on Martian Rover Software | last=Brat | first=Guillaume | publisher=Formal Methods in System Design | year=2004 | url=http://www.springerlink.com/content/r50r712p05432703/ | accessdate=2010-08-13 }}{{Dead link|date=2020年2月 |bot=InternetArchiveBot |fix-attempted=yes }}</ref><ref name="toyota_exponent">{{cite web | title=Exponent's Investigation of Toyota ETCS-i Vehicle Hardware and Software | last=Exponent | first= | publisher=Exponent | date=2012-09-24 | url=http://pressroom.toyota.com/article_download.cfm?article_id=3597 | accessdate=2010-09-07 | archive-url=https://web.archive.org/web/20140727010643/http://pressroom.toyota.com/article_download.cfm?article_id=3597 | archive-date=2014-07-27 | dead-url=yes }}</ref>。

Polyspace亦可檢查Coding Standard，如MISRA C/C++、SEI CERT C/C++、AUTOSAR C++之類的程式碼標準及指南會試著提昇程式的品質、可攜性及可靠度。Polyspace會確認C及C++的原始碼是否符合這些程式碼標準中的特定一部份規則<ref>MathWorks: [http://www.mathworks.com/discovery/static-code-analysis.html static code analysis] {{Wayback|url=http://www.mathworks.com/discovery/static-code-analysis.html |date=20170519222844 }}.</ref>。

另外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)，例如原始碼中的註解密度、[[循環複雜度]]、代碼行數、參數、函式的呼叫層級、程式中已找到的軟體錯誤等<ref>{{cite web |title=Software Metrics-MATLAB |location=India |publisher=MathWorks |url=http://in.mathworks.com/discovery/software-metrics.html |accessdate=2015-08-27 |archive-date=2016-04-02 |archive-url=https://web.archive.org/web/20160402071404/http://in.mathworks.com/discovery/software-metrics.html |dead-url=no }}</ref>。
*Polyspace Code Prover 會將原始碼用顏色編碼方案標示(紅色：會產生RTE、綠色：不會產生RTE、橘色：可能產生RTE、灰色：Dead code程式碼不會執行)，表示原始碼中不同元素的狀態<ref>{{cite web | title=A Formal Methods-based verification approach to medical device software analysis | last1=Jones | first1=Paul | last2=Jetley | first2=Raoul | last3=Abraham | first3=Jay | publisher=Embedded Systems Design | date=2010-02-09 | url=http://www.embedded.com/design/prototyping-and-development/4008888/A-Formal-Methods-based-verification-approach-to-medical-device-software-analysis | accessdate=2010-08-16 | archive-date=2014-07-25 | archive-url=https://web.archive.org/web/20140725211734/http://www.embedded.com/design/prototyping-and-development/4008888/A-Formal-Methods-based-verification-approach-to-medical-device-software-analysis | dead-url=no }}</ref>。Code Prover會使用[[形式化方法]]（Formal Verification）為基礎的靜態代碼分析來驗證程式語言層級的程式執行情形<ref name="toyota_exponent"/>。Code Prover會考慮程式中各變數的可能的值，在每一行程式提供正常及不正常使用情形下的診斷結果<ref>{{cite web | title=Static Analysis of Dynamic Properties - Automatic Program Verification to Prove the Absence of Dynamic Runtime Errors | last=Wissing | first=Klaus | publisher=Workshop on Applied Program Analysis | date=2007-09-27 | url=http://subs.emis.de/LNI/Proceedings/Proceedings110/gi-proc-110-048.pdf | accessdate=2010-08-13 | archive-date=2011-07-18 | archive-url=https://web.archive.org/web/20110718235250/http://subs.emis.de/LNI/Proceedings/Proceedings110/gi-proc-110-048.pdf | dead-url=no }}</ref>。
*Polyspace 亦提供Client/Server的功能，可以利用Client端定義work item然後submit工作到Server端去執行。另外可以透過Access的工具得到分析的結果。

== 相關條目 ==
* {{le|靜態程序分析工具列表|List of tools for static code analysis}}

== 參考資料 ==
{{Reflist|2}}

== 外部連結 ==
* [http://www.mathworks.com/static-analysis?s_cid=wiki_polyspace_3 Mathworks - Polyspace Static Analysis]
* [http://christele.faure.pagesperso-orange.fr/AlainDeutsch.html In memory of Alain Deutsch]{{Wayback|url=http://christele.faure.pagesperso-orange.fr/AlainDeutsch.html |date=20110415084024 }} （PolySpace 技术的共同创造者）
* [https://web.archive.org/web/20030810125828/http://www.testingfaqs.org/t-static.html#polyspace Software testing FAQ]

[[Category:静态代码分析工具]]
[[Category:软件测试工具]]

Polyspace - 版本历史

imported>Wolfch 来自 2026年2月14日 (六) 15:18