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

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

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

驗(yàn)證集成了 C 代碼的模型的魯棒性

補(bǔ)充 基于模型的設(shè)計(jì)（MBD） 流程的形式化驗(yàn)證能力

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

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

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

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

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

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

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

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