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. . 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 AMD-K5* 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 Industrial-Strength 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 Floating-Point 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. The tag identifies links that are outside the NASA domain