Verifying AUTOSAR Software Components with Polyspace Code Prover

Starting in R2018a, Polyspace Code Prover™ directly supports the AUTOSAR (Automotive Open System Architecture) methodology for software development. Whatever your role in the AUTOSAR software development workflow, you can now use Polyspace Code Prover in Release 2018a as an AUTOSAR-aware static analysis tool.

Polyspace Code Prover runs static program analysis on code implementations of AUTOSAR software components. The analysis looks for possible run-time errors and mismatches between the code and the design specifications in the AUTOSAR XML (ARXML).

The AUTOSAR Methodology

The AUTOSAR methodology is a software development standard for electronic control units (ECUs) in transport systems. The methodology separates the infrastructure for communicating with ECU hardware from the application layer that implements the functionality of the ECU.

In essence, the methodology provides a set of rules so that you can develop the application layer software independently of the underlying hardware. As long you follow the AUTOSAR rules regarding interfaces for communication, the AUTOSAR run-time environment (RTE) ensures that you can use the appropriate services to deploy application software on ECU hardware.

AUTOSAR Application Layer Software Development Workflow

The AUTOSAR methodology splits the application layer software development into two parts: (1) defining the architecture and communication, and (2) writing the code implementation.

1. Defining the architecture: During the so-called contract phase of AUTOSAR software development, software architects design the software components (SWCs) that comprise the application layer. Specification documents (in XML format) define the SWCs by their ports, interfaces, and runnables. Using the AUTOSAR XML (ARXML) specifications, you can generate code stubs with header files and empty bodies of C functions that implement the software component runnables.
2. Writing the code implementation: The software developer writes the bodies of C functions that implement the software component runnables. You can also generate the functions using a high-level design tool such as Simulink. (Using Simulink, you can also generate the specifications.)

Typically, these two activities occur in different organizations (e.g., OEM and tier-1 suppliers), or they occur in separate parts of an organization and often involve different domain expertise.

The AUTOSAR methodology might make it seem as though software development is a one-way process. The software architect provides the design through ARXML specifications and the developer writes the code within those specifications. In practice, this is a two-way process where implementing a design brings to light considerations that might involve changes in the design. Consider these two situations.

• New error status codes needed: The ARXML specifications define error status codes that a runnable can return. When developing the runnable, the developer realizes the need for an error status code outside the predefined ones. However, if the developer uses this new error status code, she or he is risking violating the specifications.
• Variable goes outside constrained range at run time: The ARXML specifications define a constrained range for certain data types. The constrained range is computed from physical quantities such as vehicle speed. Whenever a runnable passes a variable with a constrained data type to other runnables, the expectation is that the variable will have a value within the specified range. However, at run time, unbeknownst to the developer, the variable might acquire a value outside that range because of one unanticipated execution path (e.g., an if statement branch in the code).

These are situations where the specifications no longer reflect the state of the code accurately. At the very least, the code needs to be corrected. 

Tools to Automate the Development Process

Wouldn’t it be nice if there was a tool designed to automatically detect these situations so that the specs or code could be fixed? It would certainly make the conversations between the software architect and developer much easier.

Wouldn’t it be nicer if that tool did not require any additional setup besides the ARXML specification documents that are already available? It would be a bonus if that tool also checked for other run-time errors such as overflow and division by zero.

The good news: The new AUTOSAR capabilities in Polyspace Code Prover provide all of this functionality, helping to automate the development process.

How Does Polyspace Code Prover Fit into an AUTOSAR Workflow?

Polyspace Code Prover runs static program analysis on the code implementation of AUTOSAR software components.

All you need to provide are the two physical folders containing ARXML specifications and the code implementation (C files). Polyspace Code Prover splits your code into modules based on the software component specifications. Each module contains the C files that implement the runnables defined in the internal behavior of one software component. Each module also contains other C files that have functions called by those runnables. 

The analysis then checks each module for:

• Mismatches with the ARXML specifications. These checks determine whether:
  • All runnables are implemented.
  • Functions implementing the runnables follow the data type specifications in the ARXML. (This check covers the previously described situation where a new error status code is needed.)
  • Rte_ functions that are used for communication with other runnables follow the data type specifications in the ARXML. (This check covers the previously described situation where a variable acquires values outside a constrained range.)

• Run-time errors. These checks aim to prove the absence of certain types of run-time errors in the bodies of the runnables (for instance, overflow).

You see the check results with the usual Polyspace colors (green if proven to be valid, red if invalid, and orange if requiring manual review). You can also navigate from the Polyspace results to the specifications.

Note that the proof uses data type definitions from the ARXML specifications for more than just the checks. It also uses them for precise ranges on runnable inputs, Rte_ function return values, and output arguments. If a data type is constrained within a certain range, the proof uses this constrained range for all variables that use the data type.

In other words, the proof is AUTOSAR-aware all the way.

You can use Polyspace Code Prover at various points in your AUTOSAR development workflow. As a software developer, you can check the code implementation of software components that you are concerned with. As a software architect, you can check if the code implementation from your supplier follows your specifications. If you want to make changes in the specifications, you can also run the tool quickly to see how much of the existing code would be impacted by your changes.

For more suggestions on workflows and other details, see the Polyspace Code Prover documentation.

References

• Official AUTOSAR Standard
• AUTOSAR Compendium (Part 1: Application & RTE), Oliver Scheid (based on AUTOSAR 4.0.3)
• Introduction to AUTOSAR: Lecture by Prof. Massimo Violante