形式化方法赋能车规级芯片底层软件开发

汽车IC制造商须随产品提供高可靠性和高性能的嵌入式软件，如AUTOSAR MCAL、设备驱动程序、CPU自检软件及固件，并符合功能安全(ISO 26262)和信息安全(ISO/SAE 21434)标准。对于其客户来说，要充分发挥半导体硬件和软件堆栈，高效开发高质量产品，这些嵌入式软件至关重要。

本次演讲将介绍，如何将形式化方法应用于源代码，分析和验证软件重要属性，包括穷举分析运行时错误。然后，我们将演示如何使用Polyspace^®分析代码，评估并促进低内存占用、高性能的代码编写，而无需折衷代码健壮性。最后，我们将介绍，在软件开发生命周期的不同阶段，如何使用Polyspace来分析考量软件的性能。