驗證功能更加完善，小到快速查找缺陷大到驗證嵌入式軟件的高完整性

中國北京 – 2013 年 9 月10日– MathWorks 近日宣布引入兩款新的代碼驗證工具以擴充其 Polyspace 產品系列：Polyspace Code Prover 和 Polyspace Bug Finder。此外，公司還于同時宣布推出 2013b 版。新增的這兩款產品提供了端到端軟件驗證功能，供早期開發階段使用，其中涵蓋了查找缺陷、檢查代碼規則以及證明不存在運行時錯誤。由此便可確保嵌入式軟件的穩健性，使其能夠以較高級別的質量和安全性運行。

Polyspace Code Prover 是一款基于形式化方法的驗證工具，用于證明代碼的正確性。負責代碼安全和認證的工程師可以使用 Polyspace Code Prover 來確定何處會發生或不會發生運行時錯誤。顏色編碼和基于證明的結果簡化了驗證任務，使得軟件開發流程更加高效和優質。此外，Polyspace Code Prover 還利用 MATLAB 平臺，使用戶可以訪問強大的 MATLAB 功能，例如穩健的計算機集群間工作分配、自動化腳本編寫、結果可視化以及認證報告生成。Polyspace Code Prover 融入了先前在 Polyspace Client for C/C++ 和 Polyspace Server for C/C++ 中提供的功能。

Polyspace Bug Finder可識別嵌入式軟件中的運行時錯誤、數據流問題以及其他缺陷。Polyspace Bug Finder 可以利用靜態分析方法來分析軟件控件、數據流以及過程間行為。此軟件還能夠查找各種缺陷，例如數值、內存以及其他編程錯誤。與傳統的人工審驗不同，Polyspace Bug Finder 使工程師可以快速識別、診斷和修復代碼缺陷，從而簡化開發流程。此工具不僅可檢查是否符合代碼規則標準（例如 MISRA 和 JSF++、自定義規則），而且能夠生成衡量代碼質量和復雜度的指標。與 Polyspace Code Prover 一樣，Polyspace Bug Finder 可利用 MATLAB 平臺進行工作分配、腳本編寫和結果可視化。這兩款產品都與 Simulink 集成在一起以便用于自動生成代碼。

MathWorks 公司的設計自動化營銷總監 Paul Barnard 說：“Polyspace 產品系列可提供全面的代碼驗證解決方案，使工程師在整個開發流程中對嵌入式軟件的質量和安全性更加充滿自信。Polyspace Bug Finder 和 Polyspace Code Prover 將靜態分析和形式化方法代碼驗證技術融于一體，可幫助工程師在開發流程早期找出缺陷，證實其軟件的關鍵環節是安全的，從而加以部署。”

上市時間

Polyspace Code Prover 和 Polyspace Bug Finder已經上市。

更多信息，請訪問：

官方網站：http://www.mathworks.com/products/new_products/latest_features.html

關注MathWorks官方中文微博  www.weibo.com/mathworks

關于 MathWorks

MathWorks 公司是數學計算軟件領域世界領先的開發商。它所推出的 MATLAB 是一種用于算法開發、數據分析、可視化和數值計算的程序設計環境，稱為“科學計算的語言”。Simulink 是一種圖形環境，可用于對多領域動態系統和嵌入式系統進行仿真和模型化
設計。全球的工程師和科學家們都依賴于MathWorks 公司所提供的這些產品系列，來加快在汽車、航空、電子、金融服務、生物醫藥以及其他行業的發明、創新及開發的步伐。MathWorks 產品也是全球眾多大學和學術機構的基本教研工具。MathWorks 創建于 1984 年，總部位于美國馬薩諸塞州的內蒂克市 (Natick, Massachusetts)，在全球15 個國家/地區擁有 2800 多名員工。有關詳細信息，請訪問 www.mathworks.cn。

###

MATLAB 和 Simulink 是 The MathWorks 的注冊商標。其他商標列表，詳見 mathworks.com/trademarks。其他產品或品牌名稱可能是其各自所有人的商標或注冊商標。