DO-333 Introduction – Formal Methods

DO-333, Formal Methods Supplement to DO-178C and DO-278A, is a 118-page guideline governing Formal Methods usage in airborne and ground-based aviation software.  Interestingly, this “Formal Methods” supplement DO-333 has been called the Voodoo Zen Master bible within avionics development.  Why such an unusual term applied in the normally staid world of avionics software ?   Well, let’s see what the Tarot cards tell us about Formal Methods …

Formal Methods are comprised of mathematically based analysis of logic design used to assess correctness of that design. But software design is based upon an infinite variety of logic expressions and a near-impossibility of fully quantifying all possible interactions within that design.  In theory, Formal Methods can undoubtedly assist the development and verification of complex programs. At the same time, there are practical limits to the application of Formal Methods. Combine these facts and most practitioners agree that Formal Methods are the least understood and most subjective of the new technologies associated with aviation-related software regulations.

To best understand Formal Methods, it is helpful to quickly recap the current safety-critical software development environment that has led to the potential need for Formal Methods.

A decade ago, most aviation software was hand-coded in higher order languages such as C, Ada, and C⁺⁺. That hand-coding was done based upon a software developer’s interpretation of textual software requirements interspersed with occasional mathematical algorithms.  There were two obvious quality-related pitfalls with this approach:

1. Textual specification (e.g. English, French Chinese, etc.) lack the expressive power necessary for robust logic development; and

Incomplete or contradictory specifications led the software developer to make assumptions, and those assumptions were a common source of software errors.

Free: Download Remaining 10+ Page Paper Here