Training - Courses

• Install course files and go over agenda
• Overview of The MathWorks
• Course setup, materials, and logistics"Big picture" view of the course.

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

• Overview of PolySpace software
• Verify code using the PolySpace Launcher
• View results using the PolySpace Viewer
• Perform remote verification using PolySpace Server™ products

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 with using the PolySpace Viewer and interpreting PolySpace results.

• Overview of abstract interpretation
• Using the PolySpace Viewer
• Analyzing the call tree
• Navigating through source code
• Interpreting PolySpace results
• Execution paths
• Variable ranges
• Viewing global variable usage in source code

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
• Global 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

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: Generate standard reports from verification results, and learn methods for creating custom reports.

• Analyzing the results directory
• Generating reports in Microsoft® Excel®
• Importing and exporting comments

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