Q&A: Formal Methods Push Toward Zero-Defect Software

This article is part of the Embedded Software Series: Enforced Coding Using Ada Contracts

Download this article in PDF format.

Safety and reliability have moved to the top of the list of critical criteria in software development. There are many ways to achieve improved safety and reliability, and one of the best is to employ formal methods.

I talked with AdaCore’s SPARK product manager, Yannick Moy, about how formal verification of software can help lead to the development of zero-defect software.

Wong: What is formal program verification?

Moy: Program verification is a demonstration, to an appropriate level of confidence, that a program is correct (i.e., that it meets its specified requirements). Usually, this is achieved by a combination of testing and reviews, although tool-supported analyses are increasingly used as well. Formal program verification relies on a mathematical analysis of the program by tools to support its conclusions.

Wong: How is it different from static analysis?

Moy: Formal program verification is a special kind of static analysis with the goal of providing mathematically based guarantees about the program analyzed. For example, formal program verification may be used to show the complete absence of run-time errors (such as division by zero and buffer overflow) in the program, or the compliance of the implementation with its intended specification.

This requires an analysis that is "sound," i.e., the verification tool can never say that there is no error when the program in fact has an error (of the kind targeted by the analysis). This is quite different from the typical use of static analysis for finding bugs, which usually takes shortcuts with program semantics in order to run faster and find only sure errors.

Wong: Formal program verification requires writing function contracts such as pre- and post-conditions, right? Do you expect programmers to be able to write these contracts?

Moy: Indeed, function contracts are at the foundation of formal program verification. There are two reasons for that. First, to verify that the implementation respects an intended specification, we need a way to precisely express this specification. Function contracts meet this requirement. Second, to apply the powerful verification techniques that can prove non-trivial properties of software, we need to focus the verification on small parts of the code. Function contracts allow the programmer to focus the verification on individual functions, one at a time.

You can write multiple contracts on a function, depending on your verification objective. If your objective is simply to verify correct data accesses, initialization, and dependencies, simple contracts are needed, such as the following:

The Global contract states that global variables Accel and Giro are inputs to the procedure Stabilize, and that global variable Rotors is both an input to and an output from the same procedure. I'm using SPARK syntax here, but other languages have similar capabilities.

If your objective is to verify absence of run-time errors, specific properties, or functional correctness, then more complex contracts are needed, such as the following:

The pre-condition introduced by Pre states that procedure Stabilize should only be called when Mode is not Off. The post-condition introduced by Post states that on exit from procedure Stabilize, if Success is true, then a given relation Delta_Change relates the input and output values of the global variable Rotors. I'm again using SPARK syntax here, but other languages have similar capabilities.

As you can see from these two examples, it is well within the capabilities of programmers to write such contracts. The first one is simply an extension of the function signature, and the second one is an extension of assertions, both of which are familiar programming language features.

Wong: Even if programmers can write contracts, there’s a cost associated with this additional development activity. How do you make up for these costs to gain from this approach overall?

Moy: There are two possible reasons for using formal program verification, one related to quality and the other related to costs. And in most cases, people do it for both. The quality argument is that formal program verification can deliver a very small defect density in your software, at a reasonable cost. The cost argument is that it can deliver the same quality as extensive testing and reviews, at a smaller cost.

Formal program verification can reduce cost in two different ways. First, the guarantees provided by formal program verification mean that you can reduce and sometimes completely eliminate other activities, such as some tests and reviews. For example, there is no need to write tests or perform reviews targeted at robustness if you use formal program verification to prove the absence of run-time errors and similar properties.

Second, the quality obtained by formal program verification means that you detect errors earlier in the development cycle, when they are cheaper to correct. For example, you get a lower pre-test defect density with formal program verification than with traditional testing-based methods, and this measure is strongly correlated with overall project cost.

Wong: What companies use these techniques today?

Moy: These techniques are mostly used in domains where software errors can be very costly, such as avionics, air traffic control, nuclear reactors, security, and defense. For example, Lockheed Martin used SPARK in 1997 for the control software of the C130J military airplane, and the UK Royal Air Force and BAE Systems have since reinforced the use of SPARK to prove critical properties of C130J control software during maintenance.