Qualified Code Verification – Code Errors | Using Qualified Tools in a DO-178C Development Process, Part 8
From the series: Using Qualified Tools in a DO-178C Development Process
Showing accuracy and consistency of source code is an objective in DO-178C. When using formal methods, DO-333 allows these objectives to be satisfied by formal analysis. Polyspace Code Prover™ is a tool that can perform formal analysis on C source code, using abstract interpretation. Polyspace Code Prover detects certain potential run-time errors in the source code. The types of errors that can be detected in the source code are: unreachable code or functions not called, numeric overflows, division by zero, invalid operation on floats, invalid shift operations, illegally dereferenced pointers, non-terminating calls or loops, and out-of-bound array index. These checks can all be analyzed in a single analysis run, with a combined report being generated for these potential errors. This report also clearly shows the line of code where the specific errors can occur. The reporting uses a color coded scheme for indicating the status of each line of code: Green indicates no bug in that line of code, gray indicates an unreachable line of code, red indicates a line of code proven to have a bug, and orange indicates a possible bug that may need further manual analysis. The DO Qualification Kit provides the necessary artifacts to qualify run-time error detection and reporting by Polyspace Code Prover. The kit also provides the evidence necessary to show soundness of the formal method, as required by DO-333.
You can also select a web site from the following list
How to Get Best Site Performance
Select the China site (in Chinese or English) for best site performance. Other MathWorks country sites are not optimized for visits from your location.