ABSTRACT
Formal methods provide powerful tools and techniques for modeling and analyzing software designs and implementations. They make use of mathematics and formal logic to achieve high levels of assurance that software components have important behavioral properties or will not raise runtime errors. Since the publication of the first edition of the Digital Avionics Handbook, the field of formal methods has experienced substantial growth. This growth has occurred in core technical capabilities, in the maturity and variety of software tools, and in adoption by engineers across several industries. While the technology of formal methods has advanced steadily, more recent developments of note concern avionics certification guidance. Opportunities to use the results of formal analysis in certification are on the rise. Historically, deductive techniques were the original formal methods, dating back to the late 1960s. The other types of formal methods were introduced later in response to theoretical advances that made them possible.
