關(guān)于Polyspace應(yīng)用到基于模型的設(shè)計可能性分析和介紹

Polyspace 自 2013b 版本起開始集成到 MATLAB 平臺，利用其強大的靜態(tài)分析和形式化驗證功能完善基于模型設(shè)計的過程，同時 MATLAB 的腳本處理能力也加強了驗證的自動化過程，應(yīng)用場景包括：

獲取生成代碼的規(guī)范符合性和復(fù)雜度信息

驗證集成了 C 代碼的模型的魯棒性

補充 基于模型的設(shè)計（MBD） 流程的形式化驗證能力

以下案例說明了在基于模型的設(shè)計中 Polyspace 的可能的應(yīng)用過程。

下圖案例模型中，既包含了 Simulink 和 Stateflow 模塊，也包含了 C 代碼封裝的 s-function 函數(shù) PedalCmdLookup_C。對于這種混合代碼模型，Polyspace 可以起到很好的分析和驗證作用。

模型生成代碼之后，可以按照如下方法從 Simulink 直接調(diào)用 Polyspace，在調(diào)用之前也可以在 Option 選項中設(shè)置 Polyspace 選項。

在 Bug Finder 的結(jié)果中,可以得到違反 MISRA 規(guī)則的生成代碼（左圖）和分析得到的軟件錯誤（右圖）。

Polyspace 結(jié)果和 Simulink 模型的雙向追溯功能可以快速定位到模型中問題模塊。

對于 Sum 模塊的 MISRA 10.3 違規(guī)是為了滿足 S 函數(shù)接口要求有意為之，我們可以在驗證之前就在模型中添加說明，相應(yīng)的說明會反應(yīng)到 Polyspace 的結(jié)果中（左圖），避免了重復(fù)評審的工作；而對于指針越界的軟件錯誤，經(jīng)過分析確實是 S 函數(shù) C 代碼中的設(shè)計問題，及時修正（右圖）避免將問題留到后續(xù)環(huán)節(jié)。

同時我們還能得到生成代碼的度量信息，如圈復(fù)雜度、局部變量內(nèi)存占用情況等（左圖），用以評估模型架構(gòu)設(shè)計是否合理。Bug Finder 的“邊設(shè)計邊檢查”模式可以在設(shè)計早期就獲得高質(zhì)量的模型。

在模塊交付之前，按同樣的方法也可以調(diào)用 Code Prover，確保生成代碼中不存在運行錯誤，按此方法創(chuàng)建驗證工程的過程中由于可以繼承 Simulink 模型中數(shù)據(jù)的范圍信息（上圖右），保證了驗證的精確性。Code Prover 深度的形式化驗證能力可以發(fā)現(xiàn)更加隱蔽的問題，并且給出充分的程序調(diào)用棧信息幫助快速定位問題原因：