用Polyspace Code Prover验证AUTOSAR软件组件

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

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

AUTOSAR方法

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

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

AUTOSAR应用层软件开发工作流

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

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

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

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

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

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

自动化开发过程的工具

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

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

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

Polyspace代码证明如何适合AUTOSAR工作流?

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

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

然后分析检查每个模块:

• 与ARXML规范不匹配。这些检查确定是否:
  • 实现了所有可运行对象。
  • 实现可运行程序的函数遵循ARXML中的数据类型规范。(该检查涵盖了前面描述的需要新的错误状态代码的情况。)
  • Rte_用于与其他可运行程序通信的函数遵循ARXML中的数据类型规范。(该检查涵盖了前面描述的变量在约束范围之外获取值的情况。)

• 运行时错误。这些检查旨在证明可运行对象的主体中不存在某些类型的运行时错误(例如，溢出)。

您将看到带有通常Polyspace颜色的检查结果(绿色表示证明有效，红色表示无效，橙色表示需要手动检查)。您还可以从Polyspace结果导航到规范。

注意，证明使用ARXML规范中的数据类型定义，而不仅仅用于检查。它还将它们用于可运行输入的精确范围，Rte_函数返回值和输出参数。如果某个数据类型被限制在某个范围内，则证明将这个限制范围用于使用该数据类型的所有变量。

换句话说，证明是自动识别的。

您可以在AUTOSAR开发工作流中的不同位置使用Polyspace Code Prover。作为软件开发人员，您可以检查所关心的软件组件的代码实现。作为软件架构师，您可以检查来自供应商的代码实现是否符合您的规范。如果您希望对规范进行更改，还可以快速运行该工具，以查看您的更改会对现有代码产生多大影响。

有关工作流和其他详细信息的更多建议，请参见Polyspace Code Prover文档．

参考文献

• 官方AUTOSAR标准
• AUTOSAR纲要(第1部分:应用和RTE)， Oliver Scheid(基于AUTOSAR 4.0.3)
• AUTOSAR简介:Massimo Violante教授讲课