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

由Anirban Gangopadhyay

从R2018A开始，PolySpace Code Prover™直接支持自动开发的软件开发方法的Auto金宝appSAR（汽车开放系统架构）方法。无论您在AutoSAR软件开发工作流程中的角色，您现在都可以在2018年发布中使用PolySpace代码先驱作为AutoSAR感知静态分析工具。

Polyspace代码谚语在AutoSAR软件组件的代码实现上运行静态程序分析。分析在AutoSAR XML（ARXML）中的代码和设计规范之间进行了可能的运行时错误和不匹配。

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

图示了ECU硬件的应用分离的图。

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

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

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

通常，这两个活动发生在不同的组织（例如，OEM和Tier-1供应商）中，或者它们发生在组织的独立部分中，并且通常涉及不同的域专业知识。

AutoSAR方法可能使软件开发似乎是单向进程。软件架构师通过ARXML规范提供设计，并且开发人员将代码写入这些规范中。在实践中，这是一种双向过程，其中实现了一种设计，以指示可能涉及设计变化的考虑。考虑这两种情况。

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

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

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

如果该工具在已有的ARXML规范文档除了已有的ARXML规范文档之外，该工具是否不需要更好地更好？如果该工具还检查其他运行时误差，例如溢出和分割零零，这将是一个奖励。

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

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

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

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

然后，分析检查每个模块：

与ARXML规范不匹配。这些检查决定是否:
- 所有Runnables都已实现。
- 实现Runnable的函数遵循ARXML中的数据类型规范。（此检查涵盖了先前描述的情况，其中需要新的错误状态代码。）
- Rte_用于与其他Runnables进行通信的函数遵循ARXML中的数据类型规范。（此检查涵盖了先前描述的情况，其中变量获取约束范围之外的值。）