Quantcast

Polyspace Code Prover

Polyspace Code Verification for Fuel Rate Controller Model

In this example, you will learn how Polyspace code verification products prove code correctness, find run-time errors, and check MISRA-C:2004 compliance on generated and hand-written code.

Contents

Example Overview

This example shows how Polyspace code verification products help you achieving the following tasks

  • Prove code correctness on the integrated generated and hand-written code
  • Find run-time errors that no other tool guarantees to find
  • Check MISRA-C:2004 compliancy on legacy code

Generating the Code

Before running the Polyspace products, you need to generate code from your model. Prior to generating the code, you need to define the scope of the code verification and apply the following settings in Embedded Coder.

  • Do not generate the main function: If the subsystem is a reusable component, we want it to be verified out of this working context, without any connection with other software components
  • Generate code only for controller: We want to verify the controller code that will be embedded on the target, not the test bench used in the model.

We can simulate the model and verify that the functional behavior is as expected. We then generate the code for the controller that interfaces with the legacy code.

Once you have confidence in the functionality of the model, you can start the code verification process. The goal is to prove the correctness of the code. To do so, we need to make sure the code will behave correctly under all types of situations. We will do this without executing the code by running the Polyspace Code Prover.

Software Component Verification using Polyspace Code Prover

Once you start the Polyspace verification process with the Polyspace Code Prover, you will first see two sets of outputs in your command window.

The first output highlights errors found using the MISRA-C:2004 rules as shown in the following illustration. Depending on the MISRA policy applied to your project, you might decide to fix or ignore some errors. Alternatively, you can enable or disable specific MISRA-C:2004 rules from a graphical interface included in the Polyspace Code Prover.

The second set of output shows the dynamic range of input data extracted from the model. Two choices are available:

  • Block design min/max: The expected input values. If you only want to verify the code correctness within the existing design, you should use this mode.
  • Full range of data type: The worst case values. If you want to reuse the component in another system, for example using model reference, the expected inputs may change. Therefore, you should test using this mode.

In this example, we will use the block design min/max values for the code verification process. These block min/max values were determined from requirements made for the unit. Using the worst case values may lead to different verification results.

Opening Code Verification Results

We can use the Polyspace Code Prover GUI to see the results of our code verification process.

The GUI shows the list of C-files, including generated and legacy code, and highlights the number of checks categorized using the following colors:

  1. Green (proven code): This code section cannot contain any runtime error under the data constraints provided.
  2. Orange (possible error): This code section contains unproven code and may fail with certain values of the data constraints provided.
  3. Red (verified error): This code section will always fail under the set of data constraints provided.
  4. Gray (unreachable code): This code section cannot be reached under the data constraints provided.

For this model, we have code correctness of about 97%. We can improve upon this rate by reviewing some checks. To determine the number of checks to be reviewed and the order in which to review the checks, we can use the Methodological assistant by pressing a simple button.

When investigating the source of the checks, there are two methods:

  • Browse the code: You can first look for the cause of the error on the code level using the Code Prover GUI, then click on the code-to-model link to trace back to the model.
  • Browse the model: You can first click on the code-to-model link to trace back to the model, and then look for the cause of the error on a model level within Simulink technical computing software.

You can also do a combination of both methods.

Reviewing and Understanding Verification Results

Checks may or may not be an issue. When reviewing results, we will:

  • Increase the confidence in the code correctness
  • Increase the number of detected errors

The following shows an example of proven code:

Fixing Errors by Modifying the Model

The checks can highlight any of the following types of errors:

  • Arithmetic errors: Includes overflows, division by zero, bit-shifts, and square root of negative numbers
  • Memory corruption: Includes out-of-bound array indexes, and pointer arithmetic
  • Data truncation: Includes overflow and data wrap around
  • Coding errors: Includes non-initialized data, dead code leading to unreachable transitions or states
  • Run-time errors in legacy code: Includes pointer outside the bounds of an object, or array index pointing out of an array

When tracing back to the model, the above errors may be caused by any of the following:

  • Faulty scaling, changes in or unknown calibrations, untested data ranges coming out of a subsystem into an arithmetic block
  • Array manipulation in Stateflow event-based modeling software, hand-written look-up table functions
  • Saturations leading to unexpected data flow inside the generated code
  • Faulty Stateflow programming

Once you identify the cause of the error, you can modify the model appropriately to fix the issue.

Prerequisites to Run the Example

To run this example, you need the following products to be installed

  • Polyspace Bug Finder
  • Polyspace Code Prover
  • Embedded Coder