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

獲取生成代碼的規范符合性和復雜度信息

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

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

以下案例說明了在基于模型的設計中 Polyspace 的可能的應用過程。

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

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

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

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

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

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

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