在当前汽车产业快速发展的背景下，软件的安全与可靠性成为关键的竞争力和发展瓶颈。传统的机械汽车正在逐步被智能、自动驾驶汽车所替代，软件功能和安全要求不断提升，安全标准ISO-26262作为汽车电子电气系统的功能安全认证标准，面临着前所未有的挑战和需求。近期，高完整性软件工具专家AdaCore与全球领先的人工智能计算平台公司英伟达（NVIDIA）联合宣布，携手推动Ada和SPARK两种编程语言正式进入汽车ISO-26262市场，为自动驾驶等高安全性软件开发带来了新的解决方案。这一合作不仅凸显了Ada和SPARK在安全关键系统领域的优势，也为汽车行业的软件开发树立了标杆。英伟达的Drive® OS作为自动驾驶领域的参考操作系统，为基于DRIVE AGX硬件开发自主车辆应用提供软件基础，其软件栈中包含了多个符合ISO-26262最高完整性等级的软件组件。为了实现严格的功能安全，英伟达选择了Ada和SPARK作为部分最关键组件的开发语言。
这两种语言以其强类型、安全性和形式化验证能力，成为保障软件质量和安全的理想选择。通过结合形式化方法和Ada/SPARK的语言特性，英伟达建立了一套创新的开发流程，大幅提升了代码的可验证性和安全性。这不仅降低了软件中的潜在缺陷，还提高了在汽车安全标准认证流程中的合规效率。作为合作的一部分，AdaCore和英伟达共同将这套参照流程作为开源项目在GitHub公开，允许行业内的开发者免费使用和自由定制。这种开放策略不仅促进了生态系统的建设，也加速了Ada和SPARK语言在汽车安全软件开发中的广泛应用。该参考流程详细涵盖了软件开发生命周期的各个阶段，结合了形式验证、静态分析和安全编码规范，能够满足汽车行业日益严格的安全需求。
Ada语言诞生于20世纪70年代，专为嵌入式系统和实时高安全领域设计，具有高度的可靠性和强类型系统。SPARK则是在Ada基础上发展而来的，可以通过形式化证明手段确保软件行为符合设计规范。两者在航空航天、防务等高安全行业已有广泛应用，此次进入汽车领域，标志着其技术价值的再次升华。英伟达在自动驾驶计算平台的开发中，面临着极高的安全风险和复杂的软件系统架构。将Ada和SPARK赋能给Drive OS及周边软件组件，有效提升了系统的整体安全性能，确保自动驾驶系统能够在各种复杂环境下稳定运行。这对于未来无人驾驶技术的商业化落地和法规合规具有深远影响。
汽车行业环境复杂，软件故障可能造成严重安全事故，遵循ISO-26262标准成为行业共识。Ada和SPARK的引入不仅适应了这一趋势，更通过形式化验证和严密的语言特性，为软件开发流程带来了创新保障。AdaCore首席产品与营收官Quentin Ochem指出，随着汽车附加值逐渐向软件特性转变，实现最高级别的软件安全成为现代汽车开发最关键的挑战之一。这种联合创新体现了英伟达在技术领导力方面的卓越表现，也推动了行业的安全标准升级。除了推动产品技术，AdaCore还通过互动平台推广Ada和SPARK语言学习，辅助开发者掌握高完整性的开发技术，进一步丰富了产业人才储备。汽车软件开发者、系统集成商与汽车制造商均可利用开源文档及工具，结合自身需求快速适配和应用，促进技术普及与创新。
总的来说，Ada与SPARK携手英伟达迈入汽车ISO-26262市场，是高安全性软件开发领域的重大突破。借助开源参考流程和形式化开发优势，行业生态将获得显著优化，汽车软件的安全性和可靠性实现质的飞跃。随着智能汽车和自动驾驶技术迅猛发展，采用Ada和SPARK等先进语言和方法将成为确保生命安全与行业合规的关键路径。未来，这一合作模式与技术推广或将引领更多软件安全创新，为汽车产业带来更高水平的功能安全保障和市场竞争力。
