Objective: Become familiar with Polyspace software and work through an introductory example.

• Overview of Polyspace software
• Simple verification example
• Remote verification using Polyspace Server™

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

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

Objective: Become proficient at interpreting Polyspace results.

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

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
• 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
• Data range specifications

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

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

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
• Using the Automatic Orange Tester
• Prioritizing orange checks
• Reviewing orange checks
• Using Assistant Mode

Objective: Use the PolySpace Launcher 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
• Effects of MISRA C standards on PolySpace verification

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

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