Increasingly, we are asked to entrust our safety and even our lives to computer software.  In the Boeing 777 aircraft, there is no direct mechanical link between the pilots' controls and the aircraft's control surfaces and engines.  Instead, software reads the positions of the pilots' controls, and then commands the aircraft control surfaces to make the appropriate movements.  What if the software issues the wrong commands?  If your car has an antilock brake system, when you apply the brakes it is designed to release the brakes on individual wheels momentarily to prevent skids.  What if the ABS system should release all the brakes for a substantial amount of time?  When you use the cruise control on your car, it is supposed to shut off when you touch the brake.  What if it doesn't?

Should you really entrust such software with your life? You should not take too much comfort in the fact that the software has been tested, for testing can only find bugs. Testing can never show that no bugs are present, and even thoroughly tested software could manifest a bug the next time it is used!

The goal of research on trusted software is to find software development methods that provide a basis for trusting the software used in safety-critical applications. Two important questions trusted software research seeks to answer are: What can be done to assure that computer software performs as intended, and how confident can we be that it does so?

As you might guess, there are different levels of trust for software (the Department of Defense defines 5 levels) depending on the criticality of the application for which the software is used. The lower levels of trust can be achieved by using good programmers and good software development processes. To achieve the highest levels, however, a software developer must use a technique called formal methods.

Formal methods are based on the concepts of algebra, logic, and mathematical proof. Simply stated, one applies formal methods to prove (mathematically) that a piece of software is correct. In contrast to testing, proving that a program is correct does guarantee the absence of bugs (provided that there are none in the specification that describes what the software does, of course).

Proving a piece of software correct is not an easy task. First, one must have a formal specification of what the piece of software is supposed to do. For a cruise control system, a part of this specification might be the English statement, ``When the brake pedal is depressed, the cruise control turns off.'' This statement can be made formal by translating it into logic:

"" t,  is_depressed(break_pedal,t) Þ is_off(cruise_control,next(t))

This formal statement says, "For every time interval t, if the brake pedal is depressed at t, then the cruise control is off at the next interval after t".

Preparing a formal specification consisting of statements like this one has several advantages. First, experts in the problem domain (automotive engineers and drivers in the case of the cruise control) can analyze the specification to confirm that it does state all the required behaviors and that the required behaviors are stated correctly. Second, the formal specification is the starting point for proving that the software implementing the control system is correct.

Traditionally, one attempts to prove that a piece of software correctly implements a specification after the software has been written. That is, a programmer reads the specification and writes a program that (he thinks) does what is required by the specification. Then someone attempts to construct a proof that the software indeed does implement the specification correctly. Proofs of correctness using this traditional approach can be phenomenally difficult (and economically infeasible), because the handwritten program may not correspond very closely to the specification. Then countless small correctness theorems have to be proved, and if the overall proof of correctness fails, one has no way of knowing if one was just not inventive enough to state and prove the required theorems, or if the program is actually incorrect.

Argonne's trusted software research has developed an approach that avoids these problems. It is based on a simple observation: if one has a correct specification and changes it in a way that preserves its correctness, the new specification remains correct. We call such a change a correctness-preserving transformation. If one can find suitable correctness-preserving transformations and apply them to a specification enough times (tens of millions of times in realistic examples), one can convert the specification into a computer program. (An over-simplified example of such a transformation is one based on the observation that ; if a specification contains an instance of , then it remains correct if that instance is replaced by .)

The Argonne approach to formal methods for trusted software development requires the investment of effort to invent and prove the necessary transformations. But this effort confers several advantages:

• The programs produced by correctness-preserving transformations are related in a traceable way to their specifications.
  
  
• One does not have to guess the small correctness theorems that need to be proved, because one just needs to prove that each simple transformation preserves correctness.
  
  
• The transformations and their proofs are independent of the particular specification being transformed; thus, one proof enables the creation of many programs.
  
  
• Last, but not least, one does not have to spend the time and money to write the program, because the transformations write the program from the specification automatically!

Using these techniques, highly trusted, provably correct software can be produced at reasonable cost in time and money, and it becomes cheaper as more is produced.

If you think about it, what I have just described is a very-high level compiler for producing trusted software from specifications. Because an ordinary Fortran, C, C++, or <insert your favorite language here> program is in fact a formal specification for the required machine code, the techniques just described can be applied to produce trusted compilers. This application of program transformations is discussed further in the May, 1999 issue of IEEE Computer.