FORMAL METHODS: OBJECTIVES, TECHNIQUES, & PERSPECTIVES

                           Gerald Luettgen

Institute for Computer Applications in Science and Engineering (ICASE)
                    NASA Langley Research Center
                          Hampton, Virginia


This talk gives an introduction to the field of Formal Methods.  

Formal Methods aims at the precise modeling of and the rigorous
mathematical reasoning about digital systems.  This is of particular
importance for the growing number of embedded systems used in
safety-critical applications, such as those employed in automotive and
avionics systems.

The rationale behind Formal Methods is closely related to that in other
engineering disciplines, e.g., fluid dynamics.  However, rather than
using numerical mathematics, Formal Methods techniques are based on
discrete mathematics, i.e., logics and deduction, as well as automata
and formal language theory.  Formal methods complement well-established
quality assurance techniques, in particular, reviews and system tests.
Calculations carried out by Formal Methods tools support system
designers in checking for inconsistencies in requirements, revealing
errors in system designs, and verifying critical portions of the
implemented system.