Polyspace是MathWorks產(chǎn)品家族的一員, 也許有人還不知道它能做什么以及作用原理是什么。簡(jiǎn)單來(lái)說(shuō)，Polyspace是基于抽象解釋原理的代碼級(jí)靜態(tài)分析和驗(yàn)證工具。

的確，由于時(shí)間和成本的關(guān)系我們不可能做窮舉測(cè)試，但并不能就此推斷我們沒(méi)有測(cè)試的工況是安全的。

以汽車行業(yè)為例，已發(fā)生的多次召回事件經(jīng)分析是因?yàn)檐浖毕萦绕涫沁\(yùn)行時(shí)錯(cuò)誤（run-time error）造成的。所謂的運(yùn)行時(shí)錯(cuò)誤，是指在通常的調(diào)試過(guò)程中需要程序運(yùn)行起來(lái)之后才可能顯現(xiàn)的錯(cuò)誤，如指針越界、數(shù)據(jù)溢出等。換句話說(shuō)，如果測(cè)試用例沒(méi)有覆蓋到特定的輸入條件時(shí)，這些問(wèn)題可能就沒(méi)有機(jī)會(huì)被發(fā)現(xiàn)。

Windows平臺(tái)下調(diào)試運(yùn)行時(shí)錯(cuò)誤發(fā)生的案例

除汽車行業(yè)以外，航空航天、鐵路、醫(yī)療等所謂高完整性系統(tǒng)行業(yè)，嵌入式軟件往往承載著系統(tǒng)大部分重要功能的實(shí)現(xiàn)，一旦發(fā)生問(wèn)題會(huì)帶來(lái)異常嚴(yán)重的后果。軟件的靜態(tài)分析作為動(dòng)態(tài)功能測(cè)試的重要補(bǔ)充，在這些行業(yè)應(yīng)用非常廣泛。

所謂的靜態(tài)分析，指在不運(yùn)行程序的情況下，基于數(shù)學(xué)方法的分析來(lái)驗(yàn)證代碼是否滿足規(guī)范性、安全性、可靠性、可維護(hù)性等指標(biāo)的一種代碼分析技術(shù)。通俗地說(shuō)，靜態(tài)分析可以通過(guò)不寫(xiě)測(cè)試用例達(dá)到動(dòng)態(tài)窮舉測(cè)試的效果，是用來(lái)提高代碼魯棒性和證明軟件安全性的重要手段。

Polyspace所采用的靜態(tài)分析方法是抽象解釋，是軟件形式化驗(yàn)證方法(Formal Verification)的一種，它在處理復(fù)雜的計(jì)算問(wèn)題或模型的過(guò)程中通過(guò)對(duì)問(wèn)題進(jìn)行近似抽象，取出其中的關(guān)鍵部分進(jìn)行分析，從而減少問(wèn)題的復(fù)雜程度。

抽象解釋

簡(jiǎn)單舉例，判斷x/(x-y)是否有除零的風(fēng)險(xiǎn)的問(wèn)題可以轉(zhuǎn)換為左下圖 x和y的取值范圍是否有可能落在y=x的紅線上。Polyspace基于程序控制結(jié)構(gòu)、函數(shù)調(diào)用關(guān)系、多任務(wù)分析等，通過(guò)復(fù)雜的數(shù)據(jù)流析取過(guò)程抽象到右下圖綠色多面空間中來(lái)判斷是否有可能落在y=x上。

Polyspace中的抽象解釋

經(jīng)Polyspace分析后的代碼結(jié)果以不同顏色表:

綠色代表為安全代碼，無(wú)需花過(guò)多精力審查；

紅色代碼問(wèn)題代碼，需要立刻解決；

灰色代表不可達(dá)代碼，需要審查是設(shè)計(jì)錯(cuò)誤還是有意為之；

橙色代表有風(fēng)險(xiǎn)代碼，需要重點(diǎn)審查。

另外還可以設(shè)定編碼規(guī)范(如MISRA)和自定義代碼風(fēng)格，違反之處以紫色顯示；同時(shí)可以看到代碼變量隨控制流的數(shù)據(jù)范圍變化情況，快速查找和定位問(wèn)題原因。

Polyspace的分析結(jié)果

不論是自動(dòng)代碼還是手寫(xiě)代碼甚或混合代碼，Polyspace可以承擔(dān)類似“質(zhì)量門(mén)”的角色，幫助查找常見(jiàn)軟件缺陷、進(jìn)行代碼規(guī)范檢查、提供軟件度量信息，更進(jìn)一步通過(guò)證明不存在運(yùn)行時(shí)錯(cuò)誤交付安全代碼，大大提高代碼審查的效率并可提供安全認(rèn)證所需的相關(guān)證據(jù)。