

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 wellformed 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 astronomicallysized state spaces associated with real systems:
 Apply formal methods to requirements and highlevel 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 lifecycle 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 gatelevel 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:
 Formal Methods Application: An Empirical Tale of Software Development (Sobel) 2002
 Correctness by Construction: Developing a Commercial Secure System (Hall and Chapman), IEEE Software Jan/Feb 2002
 A mechanically checked proof
of correctness of the AMDK5* floating point
square root microcode (Russinoff), Formal Methods in System Design 1999

The Industrial Use of Formal Methods: Was Darwin Right? (Miller) Second IEEE Workshop on Industrial Strength Formal Specification Techniques Oct 1998
 Industrial Strength Exception Freedom (Amey and Chapman) 2002
 Formal Verification In a Commercial Setting (Kurshan) Bell Laboratories DAC 97
 From Formal Models to Formally Based Methods: An Industrial Experience (Ciapessoni), ACM Transactions on Software Engineering and Methodology, Jan. 1999.
 Formal Methods: State of the Art and Future Directions (Clarke and Wing) ACM Computing Surveys 1996
 The Use of IndustrialStrength Formal Methods (Bowen and Hinchey) COMPSAC 1997
 Using Formal Methods to Develop an ATC Information System (Hall) IEEE Software, Mar. 1996.
 Airbus, Eurocopter (Esterel)
 Observations On Industrial Practice Using Formal Methods (Gerhart, Craigen, and Ralston), Proceedings 15th International Conference Software Engineering, May 1993
 Lessons Learned from Applying Formal Specification in Industry (1995) (Larsen, Fitzgerald, Brookes)
 On the Need for Practical Formal Methods (Heitmeyer)
 Formal Methods Diffusion: Prospects (Adelard) 2000
 Geoff Sutcliffe's Overview of Automated Theorem Proving
 Automated Deduction Looking Ahead (Loveland), AI Magazine, Spring 1999
 Formally Verifying IEEE Compliance of FloatingPoint Hardware (Leary, Zhao, Gerth, and Seger)Intel Technology Journal 1999
 Cost Effective Use of Formal Methods in Verification and Validation (Kuhn, Chandramouli and Butler) Foundations 2002 V&V Workshop
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.
