Video e Webinar

Using Qualified Tools in a DO-178C Development Process, Part 8: Qualified Code Verification – Code Errors

From the series: Using Qualified Tools in a DO-178C Development Process

Bill Potter, MathWorks

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.

Product Focus

Series: Using Qualified Tools in a DO-178C Development Process

Part 1: Introduction to Model-Based Development for DO-178C Learn how to use of Model-Based Design and formal methods with Simulink, Stateflow, Embedded Coder, and the DO Qualification Kit in a process compliant with DO-178C, DO-331, DO-333, and DO-330.

Part 2: Qualified Model Verification – Requirements Tracing Perform tracing from models to requirements, in compliance with DO-178C and DO-331, using Simulink Requirements, and then generate a design description document using Simulink Report Generator.

Part 3: Qualified Model Verification – Simulation Perform simulation and model coverage analysis to verify models, in compliance with DO-178C and DO-331, using Simulink Test and Simulink Coverage.

Part 4: Qualified Model Verification – Model Standards Perform static analysis to verify model standards, consistency, and accuracy, in compliance with DO-178C and DO-331, using Simulink Check.

Part 5: Qualified Model Verification – Design Errors Perform formal methods analysis to verify model consistency and accuracy, in compliance with DO-178C and DO-333, using Simulink Design Verifier.

Part 6: Qualified Code Verification – Model To Code Use Embedded Coder and Simulink Code Inspector to generate code from models and verify that translation in compliance with DO-178C and DO-331.

Part 7: Qualified Code Verification – Code Standards Use Embedded Coder and Polyspace Bug Finder to generate code from models and verify coding standards in compliance with DO-178C and DO-331.

Part 8: Qualified Code Verification – Code Errors Perform formal methods analysis to verify code consistency and accuracy, in compliance with DO-178C and DO-333, using Polyspace Code Prover.

Part 9: Qualified Test Generation Use Simulink Design Verifier and Simulink Coverage to generate tests from models and verify low-level test coverage, in compliance with DO-178C and DO-331.

Part 10: Qualified Software Testing Use processor-in-the-loop capability and code coverage analysis to verify executable object code, in compliance with DO-178C and DO-331, with Simulink Test and Simulink Coverage.

Part 11: Tool Qualification Qualify MathWorks tools in compliance with DO-178C and DO-330 using the DO Qualification Kit.

Related Products

DO Qualification Kit

Learn more about the DO Qualification Kit

Next in Series

Part 9: Qualified Test Generation

Related Videos and Webinars

Model-Based Design for DO-178C Software Development with...

Model-Based Design for DO-178C Software Development with...

Simulink for DO-178 Flight Software Development

DO-178B Certification: Automate and Streamline Using Code...

Verification Workflow for Model Based Design Using...

Checking MISRA Code Rule Compliance with Polyspace Products

Understand C/C++ Code Design with Polyspace Products

What Is Polyspace Code Prover?

Embedded Software Verification with Polyspace Products for...

Best Practices for Verification and Validation

Model-Based Design for DO-178C Software Development with...

Model-Based Design for DO-178C Software Development with...

Model-Based Design for DO-178C Software Development with...

Model-Based Design for DO-178C Software Development with...

Model-Based Design for DO-178C Software Development with...

Model-Based Design for DO-178C Software Development with...

Model-Based Design for DO-178C Software Development with...

Model-Based Design for DO-178C Software Development with...

Integrating MATLAB and C/C++, Part 3: Using C/C++ Code with...

Verification by Simulation Within the Model-Based...