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

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

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

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

上市時間

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

更多信息,，請訪問：

官方網(wǎng)站：http://www.mathworks.com/products/new_products/latest_features.html

關(guān)注MathWorks官方中文微博  www.weibo.com/mathworks