使用正式的方法验证您的设计和代码
形式化验证有助于确认您的嵌入式系统软件模型和代码的行为是否正确。形式验证方法依赖于数学上严格的过程来搜索模型或代码的可能执行路径,以识别设计中的错误。您可以对模型、生成的代码和手工代码执行正式的验证。
模型的形式化验证
规范的正式验证
使用静态代码分析和正式的验证方法,您可以使用工具来检测和证明在C/ c++或Ada编写的源代码中没有溢出、被0除、越界数组访问和其他运行时错误。您可以使用它们来执行手写或生成的嵌入式软件的代码验证。您还可以检查编码标准的遵从性,检查代码复杂性度量,并度量软件质量。
有关详细信息,请参见Polyspace®2022世界杯八强谁会赢?产品。
例子和如何
软件参考
参见:静态代码分析,仿真软件设计验证器,Polyspace产2022世界杯八强谁会赢?品,仿真软件检查,仿真软件覆盖,需求的工具箱,嵌入式系统,形式验证视频,要求tracebility,基于模型的测试