用Polyspace代码验证器验证AUTOSAR软件组件

由Anirban Gangopadhyay

从R2018a开始，Polyspace代码验证程序™ 直接支持AUTOSAR（汽车开放系统体系结构）软件金宝app开发方法。无论您在AUTOSAR软件开发工作流程中扮演什么角色，现在都可以使用2018a版中的Polyspace Code Prover作为AUTOSAR感知静态分析工具。

PolyspaceCode Prover对AUTOSAR软件组件的代码实现运行静态程序分析。分析将查找AUTOSAR XML（ARXML）中代码和设计规范之间可能存在的运行时错误和不匹配。

AUTOSAR方法是一种用于运输系统中的电子控制单元(ecu)的软件开发标准。该方法将与ECU硬件通信的基础设施与实现ECU功能的应用层分离开来。

说明应用程序与ECU硬件分离的图表。

从本质上讲，该方法提供了一组规则，以便您能够独立于底层硬件开发应用层软件。只要您遵循关于通信接口的AUTOSAR规则，AUTOSAR运行时环境(RTE)就可以确保您可以使用适当的服务在ECU硬件上部署应用程序软件。

AUTOSAR方法将应用层软件开发分为两部分:(1)定义架构和通信，(2)编写代码实现。

定义架构:在AUTOSAR软件开发的所谓合同阶段，软件架构师设计组成应用层的软件组件(swc)。规范文档(XML格式)通过端口、接口和可运行对象定义swc。使用AUTOSAR XML (ARXML)规范，您可以生成带有头文件的代码存根和实现软件组件可运行项的C函数的空函数体。
编写代码实现:软件开发人员编写实现软件组件可运行对象的C函数体。您还可以使用高级设计工具(如Simulink)生成函数。金宝app(使用Simu金宝applink，您也可以生成规范。)

通常，这两种活动发生在不同的组织中(例如，OEM和一级供应商)，或者它们发生在组织的不同部分，通常涉及不同的领域专业知识。

AUTOSAR方法可能使软件开发看起来像是一个单向的过程。软件架构师通过ARXML规范提供设计，开发人员根据这些规范编写代码。在实践中，这是一个双向的过程，在实现设计的过程中，可能会涉及到设计中的更改。考虑以下两种情况。

需要新的错误状态码:ARXML规范定义了可运行对象可以返回的错误状态码。在开发可运行代码时，开发人员意识到需要预定义错误状态代码之外的错误状态代码。但是，如果开发人员使用这个新的错误状态代码，那么她或他就有违反规范的风险。
变量在运行时超出约束范围:ARXML规范为某些数据类型定义了一个受约束的范围。约束范围是由诸如车速等物理量计算得出的。当一个可运行对象将一个受约束的数据类型的变量传递给其他可运行对象时，期望变量在指定的范围内有一个值。然而，在运行时，开发人员不知道的是，变量可能会获得超出该范围的值，因为有一个意料之外的执行路径(例如，代码中的if语句分支)。

在这些情况下，规范不再准确地反映代码的状态。至少，代码需要修正。

如果有一个工具可以自动检测这些情况，从而修复规范或代码，那不是很好吗?它肯定会使软件架构师和开发人员之间的对话更加容易。

如果该工具除了可用的ARXML规范文档之外不需要任何额外的设置，不是更好吗?如果该工具还能检查其他运行时错误，如溢出和除零，那就更好了。

好消息是:Polyspace Code Prover中的新AUTOSAR功能提供了所有这些功能，帮助实现开发过程的自动化。

Polyspace代码验证程序对AUTOSAR软件组件的代码实现进行静态程序分析。

您需要提供的只是两个物理文件夹，其中包含ARXML规范和代码实现(C文件)。Polyspace Code Prover根据软件组件规范将代码分成模块。每个模块都包含C文件，这些文件实现了在一个软件组件的内部行为中定义的可运行对象。每个模块还包含其他C文件，这些文件具有可运行对象调用的函数。

Polyspace Code Prover根据软件组件规范将代码划分为模块。

然后分析检查每个模块:

与ARXML规范不匹配。这些检查决定是否:
- 所有可运行对象都实现了。
- 实现可运行对象的函数遵循ARXML中的数据类型规范。(这个检查覆盖了前面描述的需要一个新的错误状态代码的情况。)
- Rte_用于与其他可运行程序通信的函数遵循ARXML中的数据类型规范。（此检查涵盖了前面描述的情况，即变量获取的值超出了约束范围。）