MATLAB & Simulink

POLYSPACE PRODUCT

Polyspace for C/C++ Code Verification
Hands-on Course with Practical Exercises

Course Highlights

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 on-site 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

Course Objectives

• Please keep me posted on the next schedule 

• Please contact me to arrange customized/ in-house training
   

The aim of the course is to provide the participants with the knowledge on using Polyscape Code Prover to do verification, diagnostic and MISRA-C Compliance checking.

Who Must Attend 

Engineers who develop software and model for embedded system target.

Prerequisites

Strong knowledge of C or C++.

Course Outline

Day 1 of 2

Polyspace Workflow Overview

Objective: Become familiar with Polyspace Bug Finder and 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 Bug Finder.

​

- Common run-time environment artifacts

- Handling processor-specific code

- Defining the execution context

- Setting target hardware information

- Analyzing and managing 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 variable

Code Verification Checks

Objective: Find run-time errors using diagnostics available in Polyspcae 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: 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

Adding Precision to Polyspace Code Prover Verifications

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

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 Bug Finder and 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