Training - Courses

PSCC: Polyspace for Code Verification

This two-day course is intended for software engineers and focuses on verifying that code is free of run-time errors. 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^® rules
Reporting

VIEW SCHEDULE and Register SHARE with Manager/Colleague

	Detailed course outline

Day 1 of 3
Introduction to Polyspace Verification	Objective: Become familiar with Polyspace software and work through an introductory example. Overview of Polyspace software Simple verification example Remote verification using Polyspace Server
Target Compilation Environment	Objective: Verify code that may not be ANSI C compliant and account for the run-time environment. Common run-time environment artifacts Handling processor-specific code Defining the execution context Setting target hardware information
Target Compilation Environment (Ada)	Objective: Verify code that may not be compliant with the standard Ada language and account for the run-time environment. Common run-time environment artifacts Handling processor-specific code Defining the execution context Setting target hardware information
Analyzing Polyspace Results	Objective: Become proficient at interpreting Polyspace results. Overview of abstract interpretation Call tree analysis Source code navigation Execution paths Variable ranges Global variable
Function Stubbing and Data Range Specifications	Objective: Learn how Polyspace products treat missing code during verification, and how to affect this behavior to produce more meaningful verifications. Robustness verification and contextual verification Function stubbing Stubbing function inputs
Function Stubbing and Data Range Specifications (Ada)	Objective: Learn how Polyspace products treat missing code during verification, and how to affect this behavior to produce more meaningful verifications. Robustness verification and contextual verification Function stubbing Stubbing function inputs

Day 2 of 3
Code Verification Checks	Objective: Find run-time errors using diagnostics available in Polyspace products. Overview of C source code checks Location of checks in source code Description of checks Relevant verification options
Code Verification Checks (Ada)	Objective: Find run-time errors using diagnostics available in Polyspace products. Overview of Ada source code checks Location of checks in source code Description of checks Relevant verification options
Managing Oranges	Objective: Handle verification results that contain large amounts of unproven checks ("oranges"). Determining verification effort Performing a quick review (PI controller example) Performing a selective orange review (PI controller example) Setting verification precision Prioritizing orange checks Reviewing orange checks Using Assistant Mode
Enforcing MISRA-C Compliance	Objective: Use Polyspace products to check for MISRA-C compliance of source code. Overview of the MISRA-C coding standard Launching the MISRA-C checker Reviewing MISRA-C checker results Understanding the effects of MISRA-C standards on Polyspace verification
Web Metrics and Reports	Objective: Use Web metrics to share and catalog verification results, and generate standard reports from verification results. Sharing results Using Web metrics Testing software quality objectives Creating documentation
Contextual Verification	Objective: Review procedures and options that are useful when verifying larger quantities of code. Setting up a contextual verification Improving the results of a contextual verification Comparing robustness and contextual verification

Day 3 of 3

Hands-on Instruction

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

Development process review
Workflow integration
Client/Server software installation
Polyspace configuration for project code
Results interpretation

Prerequisites

Strong knowledge of C, C++, or Ada

Course Length - 2 days