Showing accuracy and consistency of low-level requirements and software architecture is an objective in DO-178C. When using formal methods, DO-333 allows these objectives to be satisfied by formal analysis, which can be applied when using models for the design. Simulink Design Verifier™ is a tool that can perform formal analysis on Simulink® and Stateflow® models. One of the formal analysis features of Simulink Design Verifier is design error detection, which detects certain potential run-time errors in the design model. The types of errors that can be detected in the model are: dead logic, integer overflows, division by zero, exceeding specified minimum and maximum values of signals, and out-of-bound array accesses. The analysis for dead logic must be run separately from the other defects. A dead logic report is generated for the model and will indicate any areas of the model that have unreachable logic, thus indicating a design error. The report will clearly show the model elements that are part of the dead logic. The other possible defects can all be analyzed in a single analysis run, with a combined report being generated for those potential errors. This report also clearly shows the model elements where the specific errors can occur. The DO Qualification Kit provides the necessary artifacts to qualify design error detection and reporting by Simulink Design Verifier. The kit also provides the evidence necessary to show soundness of the formal method, as required by DO-333.
