Polyspace
Encyclopedia
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 .
, buffer overrun, division by zero
, and others could occur. Software developer
s 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.
In organizations where quality assurance is important, Polyspace is used to demonstrate with metrics that specified software quality objectives
have been met.
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.
Static code analysis
Static program analysis is the analysis of computer software that is performed without actually executing programs built from that software In most cases the analysis is performed on some version of the source code and in the other cases some form of the object code...
tool inspired by the failure of the maiden flight
Maiden flight
The maiden flight of an aircraft is the first occasion on which an aircraft leaves the ground of its own accord. This is similar to a ship's maiden voyage....
of Ariane 5
Ariane 5 Flight 501
Cluster was a constellation of four European Space Agency spacecraft which were launched on the maiden flight of the Ariane 5 rocket, Flight 501, and subsequently lost when that rocket failed to achieve orbit. The launch, which took place on Tuesday, June 4, 1996, ended in failure due to an error...
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
Abstract interpretation
In computer science, abstract interpretation is a theory of sound approximation of the semantics of computer programs, based on monotonic functions over ordered sets, especially lattices. It can be viewed as a partial execution of a computer program which gains information about its semantics In...
to detect and prove the absence of certain run-time errors in source code
Source code
In computer science, source code is text written using the format and syntax of the programming language that it is being written in. Such a language is specially designed to facilitate the work of computer programmers, who specify the actions to be performed by a computer mostly by writing source...
for the C, C++
C++
C++ is a statically typed, free-form, multi-paradigm, compiled, general-purpose programming language. It is regarded as an intermediate-level language, as it comprises a combination of both high-level and low-level language features. It was developed by Bjarne Stroustrup starting in 1979 at Bell...
, and Ada
Ada (programming language)
Ada is a structured, statically typed, imperative, wide-spectrum, and object-oriented high-level computer programming language, extended from Pascal and other languages...
programming languages. Polyspace also checks source code for adherence to MISRA C
MISRA C
MISRA C is a software development standard for the C programming language developed by MISRA . Its aims are to facilitate code safety, portability and reliability in the context of embedded systems, specifically those systems programmed in ISO C...
and other related code standards .
Common uses
Polyspace examines the source code to determine where potential run-time errors such as arithmetic overflowArithmetic overflow
The term arithmetic overflow or simply overflow has the following meanings.# In a computer, the condition that occurs when a calculation produces a result that is greater in magnitude than that which a given register or storage location can store or represent.# In a computer, the amount by which a...
, buffer overrun, division by zero
Division by zero
In mathematics, division by zero is division where the divisor is zero. Such a division can be formally expressed as a / 0 where a is the dividend . Whether this expression can be assigned a well-defined value depends upon the mathematical setting...
, and others could occur. Software developer
Software developer
A software developer is a person concerned with facets of the software development process. Their work includes researching, designing, developing, and testing software. A software developer may take part in design, computer programming, or software project management...
s and quality assurance
Quality Assurance
Quality assurance, or QA for short, is the systematic monitoring and evaluation of the various aspects of a project, service or facility to maximize the probability that minimum standards of quality are being attained by the production process...
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
MISRA C
MISRA C is a software development standard for the C programming language developed by MISRA . Its aims are to facilitate code safety, portability and reliability in the context of embedded systems, specifically those systems programmed in ISO 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.
In organizations where quality assurance is important, Polyspace is used to demonstrate with metrics that specified software quality objectives
Software quality
In the context of software engineering, software quality refers to two related but distinct notions that exist wherever quality is defined in a business context:...
have been met.
Capabilities
Polyspace 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
Polyspace uses formal methods
Formal methods
In computer science and software engineering, formal methods are a particular kind of mathematically-based techniques for the specification, development and verification of software and hardware systems...
-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.
See also
- Static code analysisStatic code analysisStatic program analysis is the analysis of computer software that is performed without actually executing programs built from that software In most cases the analysis is performed on some version of the source code and in the other cases some form of the object code...
- Abstract interpretationAbstract interpretationIn computer science, abstract interpretation is a theory of sound approximation of the semantics of computer programs, based on monotonic functions over ordered sets, especially lattices. It can be viewed as a partial execution of a computer program which gains information about its semantics In...
- List of tools for static code analysis