使用Polyspace代码验证产品

作者:Jay Abraham 文章来源:MathWorks公司 发布时间:2012-08-28
分享到


图1  AUTOSAR架构

Elektrobit的EB tresos AutoCore是一项针对汽车ECU的符合AUTOSAR标准的行业领先的软件。为确保车辆安全,我们必须验证这些AUTOSAR组件不存在溢出、被零除、数组访问越界及其他运行时错误。

EB tresos AutoCore具有成千上万个可能的软件配置,可将其部署到当前在汽车市场中使用的任何硬件上。使用边界检查软件来识别这种应用程序中的运行时错误并不充分,因为边界检查器只能检测在测试期间触发的错误,但是还需要进行许多难以实现的测试。我们转而使用Polyspace代码验证工具。Polyspace代码验证工具不需要执行代码即可识别运行时错误,这意味着我们不需要执行专门设计的测试来捕捉这些错误。在前两个月的使用中,Polyspace代码验证工具识别了97%的代码,使其不存在某些运行时错误,从而使我们专注于其余3%的代码检查和进一步测试。

验证高度可配置软件的挑战

在许多方面,EB tresos AutoCore都是OSEK每年安装在数百万ECU上的实时操作系统)的继承者。同样,EB tresos AutoCore至少需要像OSEK一样可靠。面临的挑战是,EB tresos AutoCore是更为复杂的软件,除了支持OSEK类以外,它还必须符合AUTOSAR标准并支持所有的AUTOSAR类(见图1)。

EB tresos AutoCore几乎涵盖所有的AUTOSAR模块。基础软件大约包含100000行代码。此外,EB tresos AutoCore高度可配置,具有超过15000个参数,并且许多参数都有取值范围。

虽然在具有如此多配置参数的软件中识别可能会导致运行时错误的代码是一个繁琐又困难的过程,但为了整体系统的安全,这一过程非常重要。例如,引用无效指针可能会导致ECU停止工作,从而导致突然加速、减速或其他意外行为。

过去,我们通过植入代码并执行模块测试(嵌入式软件在其中处理数千个预先确定的FlexRay或CAN数据包)来测试运行时错误。即使在使用边界检查软件对数十个硬件架构重复执行成千上万的测试以后,我们仍然无法保证已识别所有的错误,因为我们没有办法确保我们发送的测试数据包会触发代码中所有潜在的运行时错误。此外,过多的代码植入也会减慢处理速度,从而导致软件错过实时到达的数据包。


图2 代码示例显示可能包含运行时错误的行及不包含运行时错误的行,分别以橙色和绿色突出显示

Polyspace代码验证工具不需要进行代码植入,并且我们的测试会对运行时错误进行全面检查,而不是只检查特定的情形。对于每条指令,Polyspace代码验证工具都会分析每个EB tresos AutoCore变量和参数的所有可能值。

符合ISO 26262和其他标准

在确保道路车辆符合ISO 26262功能安全标准时,涉及到证明设计满足安全要求,架构准确地反映设计,是否正确地实现架构。Polyspace代码验证工具帮助我们来完成通常很耗时的第三阶段。

EB tresos AutoCore中的所有安全相关功能均已合并到模块中,这些模块为通过总线发送的消息提供内存保护或端到端保护等。每个模块中的代码都需要进行彻底的审核以识别实现问题。Polyspace代码验证工具通过以绿色突出显示没有任何运行时错误的代码行,以橙色突出显示可能包含错误的代码行,节省了大量的审核时间(见图2)。

一个EB tresos AutoCore模块有一行橙色的代码,所有其余行均为绿色。因此,我们很清楚应该将精力放在什么地方。

除了符合AUTOSAR和ISO 26262标准外,我们的代码还必须符合MISRA C。Polyspace代码验证工具检测是否存在MISRAC编码违规,从而将我们用于静态和动态代码验证的工具数量降到最低。

通过共享内存检查提高性能

EB tresos AutoCore的某些配置包含共享全局变量。同时从多个处理线程访问这些变量可能会导致不可预测的ECU行为。该问题的标准解决方案是在变量上实现关键代码段和锁定,以便一次只有一个线程可以访问这些变量。虽然这是最安全的方法,但不一定是最有效率的方法。过度使用关键代码段可能会让系统性能降级,因为在处理每个关键代码段时必须被临时禁用中断。

为了避免让系统变慢,我们必须识别哪些共享变量需要关键代码段和锁定。这在较小的模块中并不十分困难,但在完整的系统中会变得十分复杂。我们使用Polyspace代码验证工具来执行此分析并确定是否正确配置了锁定。对EB tresos AutoCore代码执行此分析后,我们找到并消除了影响系统性能的瓶颈。

现在将EB tresos AutoCore投入生产,Elektrobit的活动AUTOSAR项目数量正在快速增长。其中一个项目将辅助驾驶系统交付给一个主要的欧洲汽车制造商。

Polyspace代码验证工具能够证明,我们交付的软件不存在某些运行时错误。更重要的是,与以前相比,我们能够更快、更全面地实现验证,同时需要较少的人工审核。

收藏
赞一下
0