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:
Procedure Stabilize ( Mode : in Mode_T; Success : out Boolean) With Global => (Input => (Accel, Giro), In_Out => Rotors );
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:
Procedure Stabilize ( Mode : in Mode_T; Success : out Boolean) With Pre => Mode /= Off, Post => (if Success then Delta_Change (RotorsâOld, Rotors));
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.
As another example, Airbus used the Caveat verification system for C in 2002 to prove compliance with low-level requirements on the Airbus A380 civilian airplane, instead of unit testing. Their use of formal program verification was included as an example in the Formal Methods Supplement of the DO-178C avionics certification standard.
In the security world, Rockwell Collins adopted SPARK for its Turnstile/SecureOne cross-domain switch, and secunet uses mostly SPARK in its multilevel workstation and Muen separation kernel. In both cases, SPARK is used to prove the absence of run-time errors (as these could lead to security attacks) and also critical security properties (such as the proper use of keys and encryption).
Beyond the traditional domains of high assurance software, new domains like automotive, robotics, and medical devices are looking at formal program verification as a way to obtain high-quality software at a reasonable cost.
Wong: How about tools that provide formal program verification?
Moy: Two toolsets provide formal program verification for industrial users of C and Ada. The Frama-C toolset for C programs is developed by CEA, and TrustInSoft commercializes a variant based on the same technology. The SPARK toolset for Ada programs is co-developed and commercialized by Altran UK and AdaCore. Other academic toolsets exist around the Eiffel, Java, and C# languages.
Wong: So, there are tools for different programming languages in this list. Are they equivalent, or are there real differences between them?
Moy: All of these tools share some algorithms to create mathematical formulas from programs, and they rely on some of the same underlying automatic provers to prove the formulas. Yet, they are very different in terms of interaction and automation, which are two critical aspects of the tools’ usability. For example, an important feature for interaction is the ability of the toolset to generate counterexamples for unproved properties, and an important feature for automation is the ability to generate missing contracts for internal functions.
Another difference is the support in the programming language for specifications. For example, the fact that SPARK is based on Ada means that users benefit in SPARK from all of the features for precise type specifications, compared to users of C. This means that there is less work for users of SPARK to specify their programs in function contracts, since many simple specifications like ranges of values are already embodied in the syntax for types.
Yannick Moy is the SPARK product manager at AdaCore. He has led the development of the SPARK language and tools since 2010, and he supervised the major technology revision resulting in SPARK 2014. Yannick has presented SPARK in numerous articles and conferences, as well as online (in particular www.spark-2014.org). Previously, he worked on software source-code analyzers CodePeer, Frama-C and PolySpace Verifier C++.
The free SPARK Course on AdaCore U e-learning website.
The online SPARK User's Guide.