The verification of coding rules and the demonstration of the absence of runtime errors. These features guarantee the robustness of embedded software that must operate at the highest levels of quality and security.
Polyspace Code Prover is a formal-methods verification tool that proves code is correct. Engineers responsible for code security and certification can use Polyspace Code Prover to reliably determine where errors will or will not occur in real time. The color-coded, test-based results simplify verification tasks, leading to a more efficient and high-quality software development process. Polyspace Code Prover also leverages the MATLAB platform to provide users with access to powerful MATLAB features, such as robust job distribution across team clusters, scripting for automation, results visualization, and report generation for certification. Polyspace Code Prover incorporates the functionality previously available in Polyspace Client for C/C++ and Polyspace Server for C/C++.
Polyspace Bug Finder identifies runtime errors, data flow problems, and other defects in embedded software. Through static analysis, Polyspace Bug Finder analyzes the control, data flow, and interprocedural behavior of the software. It can detect various defects, such as numerical and memory errors, as well as other programming mistakes. Unlike traditional manual review, Polyspace Bug Finder allows engineers to quickly identify, screen, and correct code defects to accelerate the development process. This tool also checks compliance with coding rules standards such as MISRA and JSF++, as well as custom rules, and produces metrics on code quality and complexity. Like Polyspace Code Prover, Polyspace Bug Finder leverages the MATLAB platform for distributing jobs to team clusters, scripting, and visualizing results. Both products are integrated with Simulink for use with automatically generated code.
“By providing a comprehensive code verification solution, the Polyspace product family gives engineers greater confidence in the quality and security of embedded software throughout the entire development process,” says Paul Barnard, marketing director for Design Automation at MathWorks. “Polyspace Bug Finder and Polyspace Code Prover combine static analysis and code verification techniques using formal methods to help engineers detect bugs early in the design process and demonstrate that their software is secure and ready for deployment.”
Polyspace Code Prover and Polyspace Bug Finder are now available.
