關于Polyspace的靜態分析的詳細解析和應用

Polyspace是MathWorks產品家族的一員, 也許有人還不知道它能做什么以及作用原理是什么。簡單來說，Polyspace是基于抽象解釋原理的代碼級靜態分析和驗證工具。

的確，由于時間和成本的關系我們不可能做窮舉測試，但并不能就此推斷我們沒有測試的工況是安全的。

以汽車行業為例，已發生的多次召回事件經分析是因為軟件缺陷尤其是運行時錯誤（run-time error）造成的。所謂的運行時錯誤，是指在通常的調試過程中需要程序運行起來之后才可能顯現的錯誤，如指針越界、數據溢出等。換句話說，如果測試用例沒有覆蓋到特定的輸入條件時，這些問題可能就沒有機會被發現。

Windows平臺下調試運行時錯誤發生的案例

除汽車行業以外，航空航天、鐵路、醫療等所謂高完整性系統行業，嵌入式軟件往往承載著系統大部分重要功能的實現，一旦發生問題會帶來異常嚴重的后果。軟件的靜態分析作為動態功能測試的重要補充，在這些行業應用非常廣泛。

所謂的靜態分析，指在不運行程序的情況下，基于數學方法的分析來驗證代碼是否滿足規范性、安全性、可靠性、可維護性等指標的一種代碼分析技術。通俗地說，靜態分析可以通過不寫測試用例達到動態窮舉測試的效果，是用來提高代碼魯棒性和證明軟件安全性的重要手段。

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

抽象解釋

簡單舉例，判斷x/(x-y)是否有除零的風險的問題可以轉換為左下圖 x和y的取值范圍是否有可能落在y=x的紅線上。Polyspace基于程序控制結構、函數調用關系、多任務分析等，通過復雜的數據流析取過程抽象到右下圖綠色多面空間中來判斷是否有可能落在y=x上。

Polyspace中的抽象解釋

經Polyspace分析后的代碼結果以不同顏色表:

綠色代表為安全代碼，無需花過多精力審查；

紅色代碼問題代碼，需要立刻解決；

灰色代表不可達代碼，需要審查是設計錯誤還是有意為之；

橙色代表有風險代碼，需要重點審查。

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

Polyspace的分析結果

不論是自動代碼還是手寫代碼甚或混合代碼，Polyspace可以承擔類似“質量門”的角色，幫助查找常見軟件缺陷、進行代碼規范檢查、提供軟件度量信息，更進一步通過證明不存在運行時錯誤交付安全代碼，大大提高代碼審查的效率并可提供安全認證所需的相關證據。