关于Polyspace应用到基于模型的设计可能性分析和介绍

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 深度的形式化验证能力可以发现更加隐蔽的问题，并且给出充分的程序调用栈信息帮助快速定位问题原因：