ABSTRACT
The DO-333 glossary defines formal methods as follows: Descriptive notations and analytical methods used to construct, develop and reason about mathematical models of system behavior. DO-333 clarifies DO-178C's planning and development processes when formal methods are used. DO-333 explains that the plans and standards need to be developed to describe and address the formal methods approach. The major differences between DO-178C and DO-333 are in the area of verification. DO-333 modifies objectives and activities for review and analysis of high-level requirements, lowlevel requirements, software architecture, and source code to be specific to formal methods. The goal of formal methods is to bring the same mathematical basis used for other engineering disciplines to the digital world, to both software and programmable hardware. Formal methods utilize testing as well, but they also use notations and languages for rigorous analysis. DO-333, entitled Formal Methods Supplement to DO-178C and DO-278A, was recently published by RTCA.
