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)用棧信息幫助快速定位問題原因:
-
函數(shù)
+關(guān)注
關(guān)注
3文章
4263瀏覽量
62244 -
代碼
+關(guān)注
關(guān)注
30文章
4700瀏覽量
68110
發(fā)布評(píng)論請(qǐng)先 登錄
相關(guān)推薦
評(píng)論