|Stable release||R2013b / September 6, 2013|
|Type||static code analysis|
|Website||Polyspace solution page|
Polyspace is a static code analysis tool inspired by the failure of the maiden flight of Ariane 5 where a run time error resulted in destruction of the launch vehicle. It is the first example of large-scale static code analysis by abstract interpretation to detect and prove the absence of certain run-time errors in source code for the C, C++, and Ada programming languages. Polyspace also checks source code for adherence to MISRA C and other related code standards.
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.
Code standards or guidelines such as MISRA C attempt to address code quality, portability and reliability. Polyspace checks C and C++ source code for conformance to a subset of rules in these coding standards.
The Polyspace product family consists of Polyspace Code Prover and Polyspace Bug Finder. Polyspace Code Prover annotates source code with a color-coding scheme to indicate the status of each element in the code.
- Green indicates reliable code
- Red indicates faulty code causing a run-time error
- Gray indicates dead or unreachable code
- Orange indicates unproven code
- Purple indicates code rule violation
Polyspace uses formal methods-based static code analysis to verify program execution at the language level. The tool checks each code instruction by taking into account all possible values of every variable at every point in the code. This verification process provides a formal diagnostic for each operation in the code. Polyspace verifies code under normal and abnormal usage conditions.
Polyspace Bug Finder identifies software bugs by performing static program analysis on source code. It finds defects such as numerical computation, programming, memory, and other errors. Polyspace Bug Finder also produces software metrics, includes a code rule checker that can check compliance of source code to standards such as MISRA.
- Pele, Anne-Francoise (2007-04-25). "The Mathworks acquires PolySpace Technologies". EETimes. Retrieved 2010-08-13.
- The MathWorks - Polyspace - Requirements
- Deutsch, Alain (2003). "Static Verification of Dynamic Properties". ACM. Retrieved 2010-10-03.
- Brat, Guillaume (2004). "Experimental Evaluation of Verification and Validation Tools on Martian Rover Software". Formal Methods in System Design. Retrieved 2010-08-13.
- Exponent (2010-05-18). "Interim Status of Exponent's Investigation of Toyota ETCS-i Vehicle Hardware and Software". Exponent. Retrieved 2010-09-07.
- Lopes, Rui (2009-05-29). "Static Analysis Tools, a Practical Approach for Safety-Critical Software Verification". DAta Systems In Aerospace (DASIA). Retrieved 2010-08-16.
- Briand, Patrick; Brochet, Martin; Cambois, Thierry; Coutenceau, Emmanuel; Guetta, Olivier; Mainberte, Daniel; Mondot, Frederic; Munier, Patrick; Noury, Loic; Spozio, Philippe; Retailleau, Frederic (2010-05-18). "Software Quality Objectives for Source Code". Embedded Real Time Software and Systems (ERTS2). Retrieved 2010-08-25.
- 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.
- Wissing, Klaus (2007-09-27). "Static Analysis of Dynamic Properties - Automatic Program Verification to Prove the Absence of Dynamic Runtime Errors". Workshop on Applied Program Analysis. Retrieved 2010-08-13.