Skip past navigation NASA Langley Formal Methods


home

welcome

quick page

philosophy

team

research

quote

links

new?
  home > philosophy > description

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:
  • Apply formal methods to requirements and high-level designs where most of the details are abstracted away
  • Apply formal methods to only the most critical components
  • Analyze models of software and hardware where variables are discretized and ranges drastically reduced.
  • Analyze system models in a hierarchical manner that enables "divide and conquer"
  • Automate as much of the verification as possible
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. See World Wide Web Library of Formal Methods. 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.

 

  Skip past navigation  
home | welcome | quick page | philosophy | team | research | quote | links | new?
Curator and Responsible NASA Official: Ricky W. Butler
larc privacy statement
last modified: 6 August 2001 (14:18:23)