RTCA DO-333 / EUROCAE ED-216 — Formal Methods Supplement to DO-178C

DO-333

Section 07: The Big Standards Map

Definition

A supplement to DO-178C that provides guidance for the use of formal methods in airborne software development and verification. Formal methods use mathematically rigorous techniques to specify, develop, and verify software. DO-333 allows certain DO-178C objectives to be satisfied through formal analysis rather than through testing, provided the formal analysis is demonstrated to be sound and complete for the properties being verified. The supplement addresses formal specification, formal verification (theorem proving, model checking, abstract interpretation), and the relationship between formal analysis and traditional testing and review activities.

Where This Shows Up

Formal methods offer the potential for higher confidence in software correctness, particularly for the most safety-critical functions. DO-333 provides a pathway for using formal methods to complement or, in some cases, replace testing for specific DO-178C objectives. For example, formal proof of absence of runtime errors can satisfy robustness testing objectives. However, formal methods require specialized expertise and are typically applied selectively to the highest-criticality software.

Primary Sources

RTCA DO-333 (2011) — Formal Methods Supplement to DO-178C

The primary document defining how formal methods can be applied within the DO-178C framework.

Related Terms

RTCA DO-178C / EUROCAE ED-12C — Software Considerations in Airborne Systems and Equipment Certification (DO-178C)RTCA DO-331 / EUROCAE ED-218 — Model-Based Development and Verification Supplement to DO-178C and DO-278A (DO-331)RTCA DO-332 / EUROCAE ED-217 — Object-Oriented Technology and Related Techniques Supplement to DO-178C (DO-332)

Need help navigating certification?

Understanding the terminology is the first step. If you need expert guidance on DO-178C, DO-254, ARP4754B, or any aspect of FAA, EASA, or TCCA certification, our team is here to help.