Chapter 9 - Formal Methods

Concepts of Formal Methods

Formal methods applies mathematically based principles, representations, and tools to software engineering. For centuries, bridges were built of wood and stone and were designed by experienced artisans. When iron was introduced, the venerable rules-of-thumb and intuitions were no longer valid. Bridges fell down so often that the saying arose, "Cross an iron bridge, take your life in your hands." Today Civil Engineers have a huge background of researched and mathematically sound analysis methods to design structures. Are we artisans or engineers?

Just like learning calculus, formal methods require discipline to learn the language and operation. But also like calculus, one can compute things which are difficult or impossible to measure. (The tale of Edison and the volume of the light bulb.)

Where do Formal Methods Fit in?

There are three parts to quality software production:

1. Disciplined production: analysis, requirements, design, review, version control, etc.
2. Testing and validation: is what I got, what I wanted?
3. Verification: mathematical proofs that the implementation satisfies the specification.

Formal methods may be applied at several parts of the software engineering cycle:

• requirements: formal descriptions can be checked for completeness and consistency. Formal descriptions are unambiguous, too.
• design: behavioral design languages and interface design languages.
• review: verification (program proofs) of correspondence
• implementation: program derivation or step-wise refinement from specifications to executable implementation. Also called correctness by construction.

Formal methods require more up-front work, but may greatly reduce testing time and subsequent rework.

Some Formal Methods

Analysis

OSA

Specification

Z (pronounced "zed"), BNF, Vienna development method (VDM), Communicating Sequential Processes (CSP), and Gypsy.

Interface

Larch

Proof Systems

HOL, LCF, Boyer-Moore, etc.

Links to Formal Method Sites

• Safety-Critical Systems from the World-Wide Web Virtual Library
• Searchable archive of RISKS, the Forum On Risks To The Public In Computers And Related Systems.
• A page of Formal Method Sites.