MATLAB and Simulink Training

Polyspace for C/C++ Code Verification

Course Details

This two-day course discusses the use of Polyspace® Code Prover™ to prove code correctness, improve software quality metrics, and ensure product integrity. This hands-on course is intended for engineers who develop software or models targeting embedded systems. Note that day 3 is optional and is only available for private trainings

Topics include:

  • Creating a verification project
  • Reviewing and understanding verification results
  • Emulating target execution environments
  • Handling missing functions and data
  • Managing unproven code (color-coded in orange by Polyspace products)
  • Applying MISRA-C® rules
  • Reporting analysis results

Day 1 of 2


Polyspace Workflow Overview

Objective: Become familiar with Polyspace Bug Finder and Polyspace Code Prover and work through an introductory example.

  • Software development workflows with Polyspace
  • Simple verification example
  • Analyzing defects and run-time errors

Polyspace Bug Finder Analysis

Objective: Analyze code that may not be ANSI C compliant and account for the run-time environment, and correct defects and coding rule violations using Polyspace Bug Finder.

  • Common run-time environment artifacts
  • Handling processor-specific code
  • Defining the execution context
  • Setting target hardware information
  • Analyzing and managing Polyspace Bug Finder defects
  • Detecting coding rule violations
  • Measuring code metrics

Analyzing Polyspace Code Prover Results

Objective: Become proficient at interpreting Polyspace Code Prover results.

  • Overview of abstract interpretation
  • Call tree analysis
  • Source code navigation
  • Execution paths
  • Variable ranges
  • Global variables

Code Verification Checks

Objective: Find run-time errors using diagnostics available in Polyspace Code Prover.

  • Overview of C source code checks
  • Location of checks in source code
  • Description of checks
  • Relevant verification options

Day 2 of 2


Managing Polyspace Code Prover Verifications and Results

Objective: Learn how Polyspace Code Prover treats missing code during verification, and how to affect this behavior to produce more meaningful verifications.

  • Robustness verification and contextual verification
  • Function stubbing
  • Data range specification
  • Manual stubbing

Adding Precision to Polyspace Code Prover Verifications

Objective: Handle verification results that contain large amounts of unproven checks.

  • Determining verification effort
  • Performing a quick review
  • Performing a selective orange review
  • Setting verification precision
  • Prioritizing orange checks
  • Reviewing orange checks

Integration Analysis

Objective: Learn how to manage verifications with increasing code complexity, and how to interpret and compare integrated analysis with robust analysis.

  • Managing code modules
  • Analyzing integration defects and rule violations with Polyspace Bug Finder and Polyspace Code Prover
  • Importing comments

Application Analysis

Objective: Review procedures and options that are useful when verifying complete applications.

  • Setting up an application verification
  • Improving the results of an application verification
  • Detecting concurrency issues
  • Comparing robustness and contextual verification
  • Creating documentation

Day 3 (optional, available with private training only)


Hands-On Instruction (Optional)

Objective: Spend time reviewing what you have learned and applying Polyspace directly to your own project. Potential topics include:

  • Polyspace Bug Finder checks
  • C++ code verification
  • Tasking and shared data analysis
  • Generated code verification
  • Development process review
  • Workflow integration
  • Client/server software installation
  • Polyspace configuration for project code
  • Results interpretation

Level: Intermediate

Prerequisites:

  • Strong knowledge of C or C++

Duration: 2 days

Languages: English, 日本語, 한국어, 中文