NASA logo

+ Contact NASA

  • + HOME
  • + TEAM
  • + LINKS

  • What is Formal Methods?

    "Formal Methods" refers to mathematically rigorous techniques and tools for the specification, design and verification of software and hardware systems. The phrase "mathematically rigorous" means that the specifications used in formal methods are well-formed statements in a mathematical logic and that the formal verifications are rigorous deductions in that logic (i.e. each step follows from a rule of inference and hence can be checked by a mechanical process.) The value of formal methods is that they provide a means to symbolically examine the entire state space of a digital design (whether hardware or software) and establish a correctness or safety property that is true for all possible inputs. However, this is rarely done in practice today (except for the critical components of safety critical systems) because of the enormous complexity of real systems. Several approaches are used to overcome the astronomically-sized state spaces associated with real systems: Although the use of mathematical logic is a unifying theme across the discipline of formal methods, there is no single best "formal method". Each application domain requires different modeling methods and different proof approaches. Furthermore, even within a particular application domain, different phases of the life-cycle may be best served by different tools and techniques. For example a theorem prover might be best used to analyze the correctness of a RTL level desription of a Fast Fourier Transform circuit, whereas algebraic derivational methods might best be used to analyze the correctness of the design refinements into a gate-level design. Therefore there are a large number of formal methods under development throughout the world. . There is a growing set of success stories in applying formal methods to real applications: Inclusion of these hyperlinks on the NASA web site should not be construed to represent endorsement of any commercial products mentioned on these external web sites. They are included to show that industry is claiming success in applying formal methods. The tag [*] identifies links that are outside the NASA domain