软件定义了我们的出行。从移动应用程序和实时地图，到越来越自动化的车辆，一行行的代码已经成为了世界交通的基础。

随着软件变得越来越复杂，出现人为错误的可能性也越来越大，从而会带来更多的安全风险。

为了保证这款至关重要的软件是安全的，NVIDIA正与AdaCore合作，AdaCore是安全和安保关键软件的开发和验证工具供应商。通过将Ada和SPARK编程语言应用到某些固件元素中，我们可以减少人为错误的可能性。

这两种语言的设计都考虑到了可靠性、稳健性和安全性。将它们用于编程可以为验证代码错误和漏洞的过程提升效率。

咨询公司VDC Research的一项研究显示，对于航空航天和汽车等拥有强大安全、可靠性和安全标准的行业，这些好处可以转化为通过增强软件验证节省近40%的成本和时间。

Ada具有多种内置功能，可以在软件生命周期的早期检测代码缺陷。这些措施减少了人为错误的可能性，并减少了开发后额外的测试和同行审查周期的需要。

SPARK是Ada的一个子集，它能够在数学上证明用该语言编写的代码是否没有错误。该证明能够定义软件应用程序的行为方式。它还可以确定执行是否符合该定义，发现一些通过其他方式没有检测到的错误或漏洞。

通过将这些语言集成到NVIDIA硬件中，最大限度地降低了软件发生故障或被利用的可能性。这种验证过程可以在开发周期中更快、更敏捷地进行，从而减少浪费。

将Ada和SPARK语言纳入NVIDIA的平台等措施，可以帮助提高汽车安全的稳健性，尤其是在汽车越来越自动化的情况下。

该软件必须与其运行的硬件具有一样的功能安全标准，并经过同样严格标准的安全专家评估。有了语言执行验证, 就可以进入开发过程并创建一个平滑的审查周期了。

NVIDIA软件安全副总裁 Daniel Rohrer 说： “自动驾驶汽车很复杂，需要软件的复杂程度超过了目前最严格的标准。Ada和SPARK为解决生态系统的关键需求带来了令人兴奋的可能性。”