Polyspace
{{Short description|Static program analysis tool}}
{{for|the computational complexity class|PSPACE}}
{{Infobox software
| name = Polyspace
| screenshot =
| caption =
| developer = MathWorks{{cite web | title=The Mathworks acquires PolySpace Technologies | last=Pele | first=Anne-Francoise | publisher=EETimes | date=2007-04-25 | url=http://www.eetimes.com/electronics-news/4187806/The-Mathworks-acquires-PolySpace-Technologies | accessdate=2010-08-13 | archive-url=https://web.archive.org/web/20120211091351/http://www.eetimes.com/electronics-news/4187806/The-Mathworks-acquires-PolySpace-Technologies | archive-date=2012-02-11 | url-status=dead }}
| latest_release_version = R2022b
| latest_release_date = {{Start date and age|2022|09|15}}
| operating_system = Cross-platform[http://www.mathworks.com/support/sysreq/current_release/polyspace/index.html?s_cid=wiki_polyspace_1 The MathWorks - Polyspace - Requirements]
| genre = static code analysis
| license = Proprietary
}}
Polyspace is a static code analysis tool for large-scale analysis by abstract interpretation to detect, or prove the absence of, certain run-time errors in source code for the C, C++, and Ada programming languages. The tool also checks source code for adherence to appropriate code standards.{{cite web | title=Static Verification of Dynamic Properties | last=Deutsch | first=Alain | publisher=Polyspace Technologies | date=2003-11-27 | url=http://nesl.ee.ucla.edu/courses/ee202a/2005f/papers/Static_Verification.pdf | accessdate=2014-05-17 | url-status=dead | archiveurl=https://web.archive.org/web/20120313084616/http://nesl.ee.ucla.edu/courses/ee202a/2005f/papers/Static_Verification.pdf | archivedate=2012-03-13}}
History
Polyspace was originally developed by the French company PolySpace Technologies, which was acquired by MathWorks in 2007.{{Cite web |last=Pelé |first=Anne-Françoise |date=2007-04-25 |title=The Mathworks acquires PolySpace Technologies |url=https://www.eetimes.com/the-mathworks-acquires-polyspace-technologies/ |access-date=2024-07-12 |website=EE Times}} The product was subsequently integrated into MATLAB.
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.{{cite journal|title=Experimental Evaluation of Verification and Validation Tools on Martian Rover Software | last=Brat | first=Guillaume | journal= Formal Methods in System Design | volume=25 | issue=2/3 | pages=167–198 | year=2004 | doi=10.1023/B:FORM.0000040027.28662.a4 | hdl=2060/20040010327 | hdl-access=free }}{{cite web | title=Exponent's Investigation of Toyota ETCS-i Vehicle Hardware and Software | last=Exponent | publisher=Exponent | date=2012-09-24 | url=http://pressroom.toyota.com/article_download.cfm?article_id=3597 | accessdate=2010-09-07 | archive-url=https://web.archive.org/web/20140727010643/http://pressroom.toyota.com/article_download.cfm?article_id=3597 | archive-date=2014-07-27 | url-status=dead }}
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.MathWorks: [http://www.mathworks.com/discovery/static-code-analysis.html static code analysis].
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.{{cite web|title=A Formal Methods-based verification approach to medical device software analysis | last1=Jones| first1=Paul| last2=Jetley | first2=Raoul | last3=Abraham | first3=Jay | publisher= Embedded Systems Design | date=2010-02-09 | url=http://www.embedded.com/design/prototyping-and-development/4008888/A-Formal-Methods-based-verification-approach-to-medical-device-software-analysis | accessdate=2010-08-16}} It 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, providing a formal diagnostic for each operation in the code under both normal and abnormal usage conditions.{{cite web|title=Static Analysis of Dynamic Properties - Automatic Program Verification to Prove the Absence of Dynamic Runtime Errors | last=Wissing | first=Klaus | publisher= Workshop on Applied Program Analysis | date=2007-09-27 | url=http://subs.emis.de/LNI/Proceedings/Proceedings110/gi-proc-110-048.pdf | accessdate=2010-08-13}}
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.{{cite web|title=Software Metrics-MATLAB |location=India | publisher= MathWorks | url=http://in.mathworks.com/discovery/software-metrics.html | accessdate=2015-08-27}}
See also
References
{{Reflist|2}}