Polyspace

For the computational complexity class, see PSPACE.
Polyspace
Developer(s) MathWorks [1]
Stable release R2016a / March 4, 2016 (2016-03-04)
Operating system Cross-platform[2]
Type static code analysis
License Proprietary
Website Polyspace solution page

Polyspace Bug Finder™ identifies run-time errors, concurrency issues, security vulnerabilities, and other defects in C and C++ embedded software. Using static analysis, Polyspace Bug Finder analyzes software control, data flow, and interprocedural behavior. By highlighting defects as soon as they are detected, it lets you triage and fix bugs early in the development process.Polyspace Bug Finder checks compliance with coding rule standards such as MISRA C®, MISRA C++, JSF++, and custom naming conventions. It generates reports consisting of bugs found, code-rule violations, and code quality metrics, including cyclomatic complexity. Polyspace Bug Finder can be used with the Eclipse™ IDE and integrated into build systems.

Polyspace Code Prover™ proves the absence of overflow, divide-by-zero, out-of-bounds array access, and certain other run-time errors in C and C++ source code. It produces results without requiring program execution, code instrumentation, or test cases. Polyspace Code Prover uses static analysis and abstract interpretation based on formal methods. You can use it on handwritten code, generated code, or a combination of the two. Each operation is color-coded to indicate whether it is free of run-time errors, proven to fail, unreachable, or unproven.[3]

Common uses

Polyspace examines the source code to determine where potential run-time errors such as arithmetic overflow, buffer overrun, division by zero, and others could occur. Software developers and quality assurance managers use this information to identify which parts of the code are faulty or proven to be reliable. Other parts of the code are marked for unproven checks and deserve individual review.[4][5]

Code standards or guidelines such as MISRA C attempt to address code quality, portability and reliability. The product checks C and C++ source code for conformance to a subset of rules in these coding standards.[6]

Capabilities

The product family consists of Polyspace Code Prover and Polyspace Bug Finder. The Code Prover module annotates source code with a color-coding scheme to indicate the status of each element in the code.[7] It uses formal methods-based static code analysis to verify program execution at the language level.[5] The tool checks each code instruction by taking into account all possible values of every variable at every point in the code, providing a formal diagnostic for each operation in the code under both normal and abnormal usage conditions.[8]

The Bug Finder module identifies software bugs by performing static program analysis on source code. It finds defects such as numerical computation, programming, memory, and other errors. It also produces software metrics such as Comment density of a source file, Cyclomatic complexity, Number of lines, parameters, call levels, etc. in a function, Identified run-time errors in the software.[9]

See also

References

  1. ↑ Pele, Anne-Francoise (2007-04-25). "The Mathworks acquires PolySpace Technologies". EETimes. Retrieved 2010-08-13.
  2. ↑ The MathWorks - Polyspace - Requirements
  3. ↑ Deutsch, Alain (27 November 2003). "Static Verification of Dynamic Properties" (PDF). The Special Interest Group on Ada (ACM SIGAda). Polyspace Technologies. Retrieved 14 April 2016.
  4. ↑ Brat, Guillaume (2004). "Experimental Evaluation of Verification and Validation Tools on Martian Rover Software". Formal Methods in System Design. Retrieved 2010-08-13.
  5. 1 2 Exponent (2012-09-24). "Exponent's Investigation of Toyota ETCS-i Vehicle Hardware and Software". Exponent. Retrieved 2010-09-07.
  6. ↑ MathWorks: static code analysis.
  7. ↑ Jones, Paul; Jetley, Raoul; Abraham, Jay (2010-02-09). "A Formal Methods-based verification approach to medical device software analysis". Embedded Systems Design. Retrieved 2010-08-16.
  8. ↑ Wissing, Klaus (2007-09-27). "Static Analysis of Dynamic Properties - Automatic Program Verification to Prove the Absence of Dynamic Runtime Errors" (PDF). Workshop on Applied Program Analysis. Retrieved 2010-08-13.
  9. ↑ "Software Metrics-MATLAB". India: MathWorks. Retrieved 2015-08-27.

External links

This article is issued from Wikipedia - version of the Thursday, April 14, 2016. The text is available under the Creative Commons Attribution/Share Alike but additional terms may apply for the media files.