Polyspace® software enhances the reliability of your Ada applications by proving code correctness and identifying run-time errors. Using advanced verification techniques, Polyspace software performs an exhaustive verification of your source code.
Polyspace software can:
Prove that your code has certain kinds of errors.
Prove that your code does not have certain kinds of errors.
Identify unreachable code.
Identify code that can have an error along some execution paths.
With this information, you know how much of your code does not contain run-time errors, and you can improve the reliability of your code by fixing the errors.
Polyspace software reduces development time by automating the verification process and helping you to efficiently review verification results. You can use it at any point in the development process, but using it during early coding phases allows you to find errors when it is less costly to fix them.
You use Polyspace software to verify Ada source code before compile time. To verify the source code, you set up verification parameters in a project, run the verification, and review the results. This process takes significantly less time than using manual methods or using tools that require you to modify code or run test cases.
Color-coding helps you to quickly identify errors. You will spend less time debugging because you can see the exact location of an error in the source code. After you fix errors, you can easily run the verification again.
Polyspace verification software helps you to use your time effectively. Because you know the parts of your code that do not have errors, you can focus on the code with proven (red code) or potential errors (orange code).
Reviewing the code that might have errors (orange code) can be time-consuming, but Polyspace software helps you with the review process. You can use filters to focus on certain types of errors or you can allow the software to identify the code that you should review.
Polyspace software makes it easy to share verification parameters and results, allowing the development team to work together to improve product reliability. Once verification parameters have been set up, developers can reuse them for other files in the same application.
Polyspace verification software supports code verification throughout the development process:
An individual developer can find and fix run-time errors during the initial coding phase.
Quality assurance can check overall reliability of an application.
Managers can monitor application reliability by generating reports from the verification results.