Accelerating the pace of engineering and science

Polyspace Code Prover

Key Features

  • Proven absence of certain run-time errors in C and C++ code
  • Color-coding of run-time errors directly in code
  • Calculation of range information for variables and function return values
  • Identification of variables that exceed specified range limits
  • Quality metrics for tracking conformance with software quality objectives
  • Web-based dashboard providing code metrics and quality status
  • Guided review-checking process for classifying results and run-time error status
  • Graphical display of variable reads and writes
Run-time error results displayed by Polyspace Code Prover.
Run-time error results displayed by Polyspace Code Prover.

Verifying C and C++ Embedded Software

Polyspace Code Prover performs code verification of C and C++ embedded software that must operate at the highest levels of quality, safety, and security. It is a sound static analysis tool that uses a formal methods technique called abstract interpretation to produce sound verification results. Polyspace Code Prover identifies where run-time errors may occur and code that is proven to be safe from run-time errors. You use Polyspace Code Prover as part of a high quality assurance process to exhaustively verify all possible combinations of inputs, paths, and variable values. Polyspace Code Prover uses color-coding to indicate the status of each element in the code. It integrates with Simulink® to offer traceability of code level run-time results back to the Simulink models.

With Polyspace Code Prover, you can:

  • Prove your code — verify that your code is free of run-time errors
  • Obtain results with no false negatives — all potential run-time errors are exhaustively identified
  • Gain confidence in the quality of your code — measure proven versus unproven code

You can access Polyspace Code Prover from the command line, graphical user interface, or via plugins to Visual Studio® and Eclipse™. You use it to support all critical activities in a software development workflow, including:

  • Detecting run-time errors such as divide by zero
  • Proving the absence of safety- and security-critical run-time errors such as buffer overflows
  • Determining variable ranges and ensuring that range limits are not violated
  • Ensuring that the appropriate software quality objectives are met
  • Tracing run-time errors to Simulink blocks or IBM® Rational® Rhapsody® models
  • Creating artifacts for certification

Polyspace Code Prover works with Polyspace Bug Finder to find safety-critical defects, such as divide by zero or security critical buffer overflows, in your source code and check compliance to coding standards such as MISRA. These products offer an end-to-end static analysis capability for early stage development use, spanning bug-finding, coding rules checking, and proof of run-time errors. This capability ensures the reliability of embedded software that must operate at the highest levels of quality and safety.

You can speed up and offload code verification to a computer cluster by submitting verification jobs with Parallel Computing Toolbox™ and the MATLAB Distributed Computing Server™.

Detecting Run-Time Errors

Polyspace Code Prover uses abstract interpretation with static code analysis to prove, identify, and diagnose run-time errors such as arithmetic overflows, divide by zero, and buffer overflows. This technique completely and comprehensively verifies all possible run-time conditions and automatically provides a diagnostic of proven, failed, unreachable, or unproven for each code operation. In the verification results produced by Polyspace Code Prover, each C or C++ operation is color-coded to indicate its status:

Green: proven free of run-time errors
Red: proven faulty each time the operation is executed
Gray: proven unreachable (may indicate a functional issue)
Orange: unproven operation may be faulty under certain conditions
Color-coded run-time error attributes identified by Polyspace Code Prover.

Run-time error attributes identified by Polyspace Code Prover.

Errors detected include:

  • Arithmetic overflows, underflows, divide-by-zero, and other arithmetic errors
  • Buffer overflows and illegally dereferenced pointers
  • Always true/false statement
  • Noninitialized class members (C++)
  • Read access to noninitialized data
  • Access to null this pointer (C++)
  • Dead code
  • Dynamic errors related to object programming, inheritance, and exception handling (C++)

Viewing Range Information

Polyspace Code Prover tracks control and data flow through the software and displays range information associated with variables and operators. By placing your cursor over an operator or variable, a tooltip message displays the range information. The formal method known as abstract interpretation enables determination of accurate range information for the purpose of proving that the software is free of certain run-time errors such as divide by zeros and buffer overflows. You can use range information to track the control and data flow precisely to debug your software or to ensure that certain variables or operations do not violate specified range limits.

In the example below, Polyspace Code Prover has determined that the division operation consists of a range between -1701 to 3276 for the left operand; right operand is 9. The resulting range after division is -189 to 364.

Tooltip displaying the possible ranges for all run time conditions.
Tooltip displaying the possible ranges for all run time conditions.

You can further visualize the control flow using the call hierarchy and the call flow graphs or view the accesses for your global variable data

Call flow graph displaying the order of function calls in an interprocedural analysis.
The order of function calls in an interprocedural analysis.
Variable ranges as a result of the data flow analysis
Variable ranges as a result of the data flow analysis.

Tracking Software Quality Metrics

You can define a centralized quality model to track run-time errors, code complexity, and coding rules violations. Using these metrics you can track your progress toward predefined software quality objectives as your code evolves from the first iteration to the ultimate delivery version. By measuring the rate of improvement in code quality, Polyspace Code Prover enables developers, testers, and project managers to target and deliver high quality code.

Software quality metrics displayed via web browser.
Software quality metrics displayed via a web browser.

Tracing Code Verification Results to Simulink Models

You can use Polyspace Code Prover to verify generated code or mixed code which contains both generated and handwritten code. Code-level defect results in the automatically generated code are traced back to the model in Simulink. You can identify which parts of the model are reliable; and correct design problems that will cause errors in the code. You can also identify potential problems between the interface of generated and handwritten code. For example, the mixing of hand-written S-Function code with generated code could result in a problem where incorrect ranges of signals in the interface cause a run-time error.

Polyspace Code Prover also supports tracing run-time results to dSPACE® TargetLink® blocks and IBM Rational Rhapsody models.

Tracing code verification results to the Simulink model.
Tracing code verification results to the Simulink model.

Automating Code Verification Process

You can use Polyspace Code Prover as part of a continuous integration process by incorporating Polyspace into your build process. You can automate verification job scheduling and set up email notifications. You can assign Polyspace Code Prover to schedule the posting of a verification job to a cluster computer (using MATLAB Distributed Computing Server), and receive email notifications when the results are available. Results contain the differences compared with the previous version of your code, which the server computes automatically.

You can define the frequency of these analyses, the quality model you want to apply for a given portion of your code base, and the emails you want your users to receive when the results are available. Also, you can define which characteristics of the build process you want the automated verifications to encompass.

Creating Certification Artifacts

You can use Polyspace Bug Finder and Polyspace Code Prover with IEC Certification Kit (for IEC 61508 and ISO 26262) and DO Qualification Kit (for DO-178B) in the certification process for projects based on these industry standards.

Reports and artifacts show the final quality of the code, highlight sections that have been reviewed, generate code metrics, and document the application of coding rules and run-time error status. You can create these reports in PDF, HTML, RTF, and other formats.

DO Qualification Kit contents.
Certification and qualification kits are available.

Mejores Prácticas para la Verificación y Validación de modelos...

View webinar