Documentation

Sample Workflows for Polyspace Verification

Overview of Verification Workflows

Polyspace® verification supports two goals at the same time:

  • Reducing the cost of testing and validation

  • Improving software quality

You can use Polyspace verification in different ways depending on your development context and quality model. The primary difference being how you exploit verification results.

This section provides sample workflows that show how to use Polyspace verification in a variety of development contexts.

Software Developers – Standard Development Process

User Description

This workflow applies to software developers using a standard development process. Before implementing Polyspace verification, these users fit the following criteria:  

  • In Ada, unit test tools or coverage tools are not used – functional tests are performed just after coding.

  • In C, either coding rules are not used, or rules are not followed consistently.

Quality

The main goal of Polyspace verification is to improve productivity while maintaining or improving software quality. Verification helps developers find and fix bugs more quickly than other processes. It also improves software quality by identifying bugs that otherwise might remain in the software.

In this process, the goal is not to completely prove the absence of errors. The goal is to deliver code of equal or better quality than other processes, while optimizing productivity to provide a predictable time frame with minimal delays and costs.

Verification Workflow

This process involves file-by-file verification immediately after coding, and again just before functional testing.

The verification workflow consists of the following steps:

  1. The project leader configures a Polyspace project to perform robustness verification, using default Polyspace options.

      Note:   This means that verification uses the automatically generated "main" function. This main will call unused procedures and functions with full range parameters.

  2. Each developer performs file-by-file verification as they write code, and reviews verification results.

  3. The developer fixes red errors and examines gray code identified by the verification.

  4. Until coding is complete, the developer repeats steps 2 and 3 as required.

  5. Once a developer considers a file complete, they perform a final verification.

  6. The developer fixes red errors, examines gray code, and performs a selective orange review.

      Note:   The goal of the selective orange review is to find as many bugs as possible within a limited period of time.

Using this approach, it is possible that some bugs may remain in unchecked oranges. However, the verification process represents a significant improvement from the previous process.

Costs and Benefits

When using verification to detect bugs:

  • Red and gray checks — The number of bugs found in red and gray checks varies, but approximately 40% of verifications reveal one or more red errors or bugs in gray code.

  • Orange checks — The time required to find one bug varies from 5 minutes to 1 hour, and is typically around 30 minutes. This represents an average of two minutes per orange check review, and a total of 20 orange checks per package in Ada and 60 orange checks per file in C.

Disadvantages to this approach:

  • Setup time — the time required to set up your verification will be higher if you do not use coding rules. You may have to make modifications to the code before starting the verification.

Software Developers – Rigorous Development Process

User Description

This workflow applies to software developers and test engineers working within development groups. These users are often developing software for embedded systems, and typically use coding rules.

These users typically want to find bugs early in the development cycle using a tool that is fast and iterative.

Quality

The goal of Polyspace verification is to improve software quality with equal or increased productivity.

Verification can prove the absence of run-time errors, while helping developers find and fix bugs more quickly than other processes.

Verification Workflow

This process involves both code analysis and code verification during the coding phase, and thorough review of verification results before module testing. It may also involve integration analysis before integration testing.

Workflow for Code Verification

    Note:   Solid arrows in the figure indicate the progression of software development activities.

The verification workflow consists of the following steps:

  1. The project leader configures a Polyspace project to perform contextual verification. This involves:

    • Creates a "main" program to model call sequence, instead of using the automatically generated main.

    • Sets options to check the properties of some output variables. For example, if a variable y is returned by a function in the file and should always be returned with a value in the range 1 to 100, then Polyspace can flag instances where that range of values might be breached.

  2. The project leader configures the project to check the required coding rules.

  3. Each developer performs file-by-file verification as they write code, and reviews both coding rule violations and verification results.

  4. The developer fixes coding rule violations, fixes red errors, examines gray code, and performs a selective orange review.

  5. Until coding is complete, the developer repeats steps 2 and 3 as required.

  6. Once a developer considers a file complete, they perform a final verification.

  7. The developer performs an exhaustive orange review on the remaining orange checks.

      Note:   The goal of the exhaustive orange review is to examine all orange checks that were not reviewed as part of previous reviews. This is possible when using coding rules because the total number of orange checks is reduced, and the remaining orange checks are likely to reveal problems with the code.

Optionally, an additional verification can be performed during the integration phase. The purpose of this additional verification is to track integration bugs, and review:

  • Red and gray integration checks;

  • The remaining orange checks with a selective review: Integration bug tracking.

Costs and Benefits

With this approach, Polyspace verification typically provides the following benefits:

  • 3–5 orange and 3 gray checks per file, yielding an average of 1 bug. Often, 2 of the orange checks represent the same bug, and another represent an anomaly.

  • Typically, each file requires two verifications before it can be checked-in to the configuration management system.

  • The average verification time is about 15 minutes.

      Note:   If the development process includes data rules that determine the data flow design, the benefits might be greater. Using data rules reduces the potential of verification finding integration bugs.

If performing the optional verification to find integration bugs, you may see the following results. On a typical 50,000 line project:

  • A selective orange review may reveal one integration bug per hour of code review.

  • Selective orange review takes about 6 hours to complete. This is long enough to review orange checks throughout the whole application and represents a step towards an exhaustive orange check review. Spending more time is unlikely to be efficient.

  • An exhaustive orange review takes between 4 and 6 days, assuming that 50,000 lines of code contains approximately 400–800 orange checks.

Quality Engineers – Code Acceptance Criteria

User Description

This workflow applies to quality engineers who work outside of software development groups, and are responsible for independent verification of software quality and adherence to standards.

These users generally receive code late in the development cycle, and may even be verifying code that is written by outside suppliers or other external companies. They are concerned with not just detecting bugs, but measuring quality over time, and developing processes to measure, control, and improve product quality going forward.

Quality

The main goal of Polyspace verification is to control and evaluate the safety of an application.

The criteria used to evaluate code can vary widely depending on the criticality of the application, from absence of red errors only to exhaustive oranges review. Typically, these criteria become increasingly stringent as a project advances from early, to intermediate, and eventually to final delivery.

For more information on defining these criteria, see Defining Software Quality Levels.

Verification Workflow

This process usually involves both code analysis and code verification before validation phase, and thorough review of verification results based on defined quality goals.

    Note:   Verification is often performed multiple times, as multiple versions of the software are delivered.

The verification workflow consists of the following steps:

  1. Quality engineering group defines clear quality goals for the code to be written, including specific quality levels for each version of the code to be delivered (first, intermediate, or final delivery) For more information, see Defining Quality Goals.

  2. Development group writes code according to established standards.

  3. Development group delivers software to the quality engineering group.

  4. The project leader configures the Polyspace project to meet the defined quality goals, as described in Defining a Verification Process to Meet Your Goals.

  5. Quality engineers perform verification on the code.

  6. Quality engineers review red errors, gray code, and the number of orange checks defined in the process.

      Note:   The number of orange checks reviewed often depends on the version of software being tested (first, intermediate, or final delivery). This can be defined by quality level (see Defining Software Quality Levels).

  7. Quality engineers create reports documenting the results of the verification, and communicate those results to the supplier.

  8. Quality engineers repeat steps 5–7 for each version of the code delivered.

Costs and Benefits

The benefits of code verification at this stage are the same as with other verification processes, but the cost of fixing faults is higher, because verification takes place late in the development cycle.

It is possible to perform an exhaustive orange review at this stage, but the cost of doing so can be high. If you want to review all orange checks at this phase, it is important to use development and verification processes that minimize the number of orange checks. This includes:

  • Developing code using strict coding and data rules.

  • Providing accurate manual stubs for unresolved function calls.

  • Using DRS to provide accurate data ranges for input variables.

Taking these steps will minimize the number of orange checks reported by the verification, and make it likely that remaining orange checks represent true issues with the software.

Project Managers — Integrating Polyspace Verification with Configuration Management Tools

User Description

This workflow applies to project managers responsible for establishing check-in criteria for code at different development stages.

Quality

The goal of Polyspace verification is to test that code meets established quality criteria before being checked in at each development stage.

Verification Workflow

The verification workflow consists of the following steps:

  1. Project manager defines quality goals, including individual quality levels for each stage of the development cycle.

  2. Project leader configures a Polyspace project to meet quality goals.

  3. Developers run verification at the following stages:

    • Daily check-in — On the files currently under development. Compilation must complete without the permissive option.

    • Pre-unit test check-in — On the files currently under development.

    • Pre-integration test check-in — On the whole project, ensuring that compilation can complete without the permissive option. This stage differs from daily check-in because link errors are highlighted.

    • Pre-build for integration test check-in — On the whole project, with multitasking aspects accounted for as required.

    • Pre-peer review check-in — On the whole project, with multitasking aspects accounted for as required.

  4. Developers review verification results for each check-in activity to confirm that the code meets the required quality level. For example, the transition criterion could be: "No bug found within 20 minutes of selective orange review"

Was this topic helpful?