验证AUTOSAR软件组件- MATLAB和Simulink - 卡塔尔世界杯8强比赛直播

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

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

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

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

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

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

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

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

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

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

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

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

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

Polyspace代码验证器在AUTOSAR软件组件的代码实现上运行静态程序分析。

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

然后分析检查每个模块:

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

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

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

换句话说，证明是完全支持autosar的。

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

有关工作流和其他详细信息的更多建议，请参见Polyspace代码证明程序文档．

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