MathWorks 引入兩款 Polyspace 代碼驗證新產(chǎn)品

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

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

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

　　MathWorks 公司的設計自動(dòng)化營(yíng)銷(xiāo)總監 Paul Barnard 說(shuō)：“Polyspace 產(chǎn)品系列可提供全面的代碼驗證解決方案，使工程師在整個(gè)開(kāi)發(fā)流程中對嵌入式軟件的質(zhì)量和安全性更加充滿(mǎn)自信。Polyspace Bug Finder 和 Polyspace Code Prover 將靜態(tài)分析和形式化方法代碼驗證技術(shù)融于一體，可幫助工程師在開(kāi)發(fā)流程早期找出缺陷，證實(shí)其軟件的關(guān)鍵環(huán)節是安全的，從而加以部署。”

　　上市時(shí)間

　　Polyspace Code Prover 和 Polyspace Bug Finder已經(jīng)上市。