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

由Anirban Gangopadhyay

从R2018a开始，Polyspace Code Prover™直接支持用于软件开发的AUTOSAR(汽金宝app车开放系统架构)方法。无论您在AUTOSAR软件开发工作流中的角色是什么，您现在都可以使用Release 2018a中的Polyspace Code Prover作为AUTOSAR感知的静态分析工具。

Polyspace代码验证程序对AUTOSAR软件组件的代码实现进行静态程序分析。分析寻找可能的运行时错误和代码与AUTOSAR XML (ARXML)中的设计规范之间的不匹配。

AUTOSAR的方法

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

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

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

AUTOSAR应用层软件开发流程

AUTOSAR方法将应用层软件开发分为两部分：（1）定义体系结构和通信，（2）编写代码实现。

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

通常，这两项活动发生在不同的组织（如OEM和一级供应商），或者发生在组织的不同部分，通常涉及不同的领域专业知识。

AUTOSAR方法可能会让人觉得软件开发是一个单向的过程。软件架构师通过ARXML规范提供设计，开发人员在这些规范中编写代码。在实践中，这是一个双向的过程，在这个过程中，实现一个设计会带来可能涉及到c在设计中悬挂。考虑这两种情况。

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

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

自动化开发过程的工具

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

如果该工具除了已经可用的ARXML规范文档之外不需要任何额外的设置，那不是更好吗？如果该工具还检查其他运行时错误（如溢出和零除），那将是一个额外的好处。

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

Polyspace代码验证程序如何适应AUTOSAR工作流？

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

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

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

然后，分析检查每个模块是否存在以下情况：

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