说明
Polyspace从2013b发行版集成到MATLAB平台中，利用其强大的静态分析和形式化验证功能完善了基于模型设计的过程，同时通过MATLAB的脚本处理能力增强了验证自动化过程。 应用场景如下。
获取生成代码的规格适用性和复杂性的信息
验证综合c码模型的鲁棒性
补充基于模型的设计(MBD )过程的形式化验证能力
以下案例说明了Polyspace在基于模型的设计中的可能应用过程。
下图中的案例模型既包含Simulink和Stateflow模块，也包含c代码包中的s-function函数PedalCmdLookup_C。 对于这种混合码模型，Polyspace可以起到很好的分析和验证作用。
在模型生成代码后，可以直接从Simulink调用Polyspace，如下所示： 也可以在调用之前在Option选项中设置Polyspace选项。
错误过滤器结果将生成违反MISRA规则的生成代码(左)和分析结果(右)。
Polyspace结果和Simulink模型的双向向下钻取功能可以快速导航到模型中的问题模块。
对Sum模块的MISRA 10.3违规是为了满足s函数接口的要求而故意进行的，可以在验证之前向模型中添加说明，相应的说明将反映在Polyspace的结果中，避免了重复的审阅工作。 (； 另一方面，指针越界的软件错误，经过分析，确实是s函数c码的设计上的问题，为了不使问题遗留在后续环节，要及时进行修正(右图)。
此外，还可以获取生成的代码的测量信息，如循环复杂性、局部变量的内存消耗等，以评估模型体系结构的设计是否合理。 Bug Finder的“边设计边检查”模式在设计初期就可以获得高质量的模型。
也可以在交付模块之前，用同样的方法调用Code Prover来确保生成的代码中没有执行错误。 通过这种方法建立验证工序的过程中，可以继承Simulink模型的数据范围信息，从而保证了验证的正确性。 Code Prover的深度形式化验证能力可以发现更隐蔽的问题，提供充分的程序调用栈信息，从而快速找出问题的原因。
打开APP阅读更多精彩内容
点击阅读全文