Polyspace Code Prover for C/C++ Code Verification
Strong knowledge of C or C++
Detailed course outline
|Day 1 of 3|
|Introduction to Polyspace Verification|
Objective: Become familiar with Polyspace Code Prover and work through an introductory example.
- Overview of Polyspace Code Prover
- Simple verification example
- Remote verification using MATLAB Distributed Computing 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
|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
|Function Stubbing and Data Range Specifications|
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
- Stubbing function inputs
|Day 2 of 3|
|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
|Managing Orange Checks|
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
- Using Assistant Mode
|Enforcing MISRA-C Compliance|
Objective: Use Polyspace 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 Code Prover 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
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|
Objective: Spend time reviewing what you have learned and applying Polyspace Code Prover directly to your own project. Potential topics include:
- Development process review
- Workflow integration
- Client/Server software installation
- Polyspace configuration for project code
- Results interpretation