LOOK into the sky above a large city and you are almost certain to see at least one aircraft skimming the edges of your field of vision. In London, it may be as many as five planes or more waiting for a landing spot at one of the city鈥檚 two main airports. With the number of air passengers in Britain expected to exceed 188 million a year by 2005, it is no surprise that the world鈥檚 major centres for air traffic control are rethinking procedures and redesigning their systems.
This was just what the Britain鈥檚 Civil Aviation Authority did in 1992 when it upgraded the London Area Terminal Control centre 鈥� and the efforts are now starting to pay off. The requirements for the new system were stringent: the traffic managers who are in direct contact with pilots during take-off and landing need up to the second information on weather, airport status, arrivals, pending departures 鈥� and all at the press of a button. Most importantly, the data they see on their screens must be accurate.
With the lives of so many thousands of people at stake each day, the software underlying a system such as the one designed for the CAA must be utterly reliable. If the software in such a system 鈥� which is often referred to as being safety critical 鈥� crashes, then there is an increased chance of some of the planes crashing as they arrive or leave the controlled air space. Designing such software requires great care and attention to detail. So the CAA, along with Praxis, a British software company, chose to use a technique known as formal methods during its design process. This relies on mathematical models of software languages rather than a 鈥渘atural鈥� language such as English to describe what the software will do. These mathematical models can then be solved to test the design.
Advertisement
With microprocessors and their accompanying software being built into more and more safety-critical systems ranging from medical appliances to car engines, designing high-quality software is more important than ever. Yet software design projects have a relatively poor record of success. Studies show that a quarter of large-scale software systems are cancelled during development and three-quarters of all large-scale systems that are developed are actually 鈥渙perating failures鈥�, that do not work properly or not at all.
Simply specify
Anthony Hall, a senior consultant at Praxis, thinks that formal methods hold out hope for improving and enhancing traditional methods of design. 鈥淲e are accumulating evidence that, used in conjunction with other good software engineering practices, formal methods can lead to higher quality with no increase in cost.鈥� They can, he says, lead to 鈥渃lear understanding of the requirements 鈥� simple design, high testability 鈥� and can help master the complexity of difficult design areas鈥�.
Other organisations have also recognised these strengths and are beginning to use formal methods in their software development projects. GEC Alsthom in Paris, for example designed the upgraded switching and control software for running their national railway system using a formal specification. Meanwhile, Formal Systems (Europe), an Oxford-based consultancy specialising in formal methods for software design, has worked with Westinghouse to verify signalling software, and Draper Laboratory, a research centre, has been funded by the American government to verify fault-tolerant computer hardware.
And in the past few years a number of organisations 鈥� such as the International Electrotechnical Commission covering European Standards and the European Space Agency 鈥� have started to recommend these design methods when putting contracts out to tender. And the Ministry of Defence in Britain and the Canadian Energy Control Board have made formal methods mandatory for their software projects.
But just what do these organisations mean when they say that they have followed a formal design and how can formal methods improve the quality of software? One of the key features of using a formal design methodology is the specification phase. Before anyone sits down to write a computer program, whether it be the microcode that controls the opening and shutting of switches on a chip, a specific program for controlling the locking of brakes on a car, or a software package for accounting, a team will get together to decide what the overall program should do.
This involves splitting up the work among a group of programmers, setting realistic deadlines and ensuring that the specified functions are included. Most specifications are written in the language spoken by the design team. During the life-cycle of the design, the specification documents become more detailed, perhaps including data flow diagrams and details of input and output values of specified functions.
In contrast, a formal specification is a series of logic equations. According to software designers such as Hall, the process of having to convert ideas into these equations is in itself a good way of clarifying and simplifying design goals. Take, for example, the design of the software needed to control an electronic checkout machine. The formal specification for this relatively simple task would look something like this:
- [Scanner (input: COST) (output: DISPLAY)
- TOTAL:= TOTAL + COST;
- DISPLAY:= VIEW TOTAL]
The English equivalent would be: display a running total of the prices of items collected using a hand-held scanner on the screen of the cash register. The register should have two buttons: one to open the drawer and one to close it. A more detailed specification might also describe how the computer must store the running total in its memory during a transaction, and there should be some way for the computer to register whether the drawer is open or closed and the scanner in use.
At first sight, the formal specification may look like computer code. The difference is that the input and output refer to what the checkout assistant will observe. The rules, or algorithms, that describe how the computer should display numbers on the screen, for example, are missing. In the formal specification, these are merely referred to by the words TOTAL and DISPLAY. The specification would also include a statement describing the data represented by TOTAL and COST 鈥� in this case a positive number. Later on, the software programmers and electronics engineers will need to be careful about converting those numbers into binary code.
The next step in the specification is to describe what happens to the drawer at various stages of the transaction. In English, the checkout assistant presses a button marked OPEN after scanning all the items. This opens the drawer. To close it, he or she presses the button marked CLOSE. This also triggers the display to be returned to zero ready for the next customer.
As a formal specification this would be written in the following manner:
[Drawer (input: OPEN, CLOSE) (output: DRAWER, DISPLAY)
if (OPEN IS PRESSED) and (DRAWER IS CLOSED)
then DRAWER:= OPEN;
if (CLOSED IS PRESSED) and (DRAWER IS OPEN)
then DRAWER:= CLOSED; TOTAL:= ZERO;
DISPLAY:=VIEW ZERO]
Both the logic specification and the English explanation may seem clear and correct. But on closer inspection, mistakes become visible. Should items, for instance, be scanned while the drawer is open? The present design allows for this kind of action, but in reality the scanner should probably be disabled while the customer is paying. To enforce this requirement a designer would encode this as the equation:
(SCANNER ENABLED) implies (DRAWER IS CLOSED)
This is called an invariant because it is a property that should always be true whatever the checkout assistant does. Invariants like these are used as guides to check the correctness of the design. Spotting errors is much easier in the mathematical specification than in the written English text because the use of invariants, for example, describe exactly the interaction between components. In this case, opening the drawer should trigger the scanner to be disabled. At this stage, a designer can see where the bug in the design is and, hopefully, they will be able to fix it before any programs are written.
But if this kind of error can be missed in a simple specification, what happens when design teams sit down to write the requirements for a program to control air traffic or a spacecraft, for example? Studies at the Jet Propulsion Laboratory have shown that two-thirds of defects can be blamed on omissions in the specification. Similar studies show that of the 197 safety-critical faults detected in the Voyager and Galileo spacecraft, only three were programming bugs, the rest resulted from flawed requirements or misinterpretation of what the user needed to do.
One way the use of a mathematical specification gets around such problems is focusing the design team鈥檚 attention on exactly what the user will do with the final system. Praxis, for example, used a formal specification to describe the whole design of the information display for the air traffic control system from a user鈥檚 point of view. The specification was restricted to equations that described processes such as what would happen when a certain button was pressed.
According to Hall, the Praxis designers found that mathematics helped by forcing them to ask lots of questions about how the users would interact with the final system, as they tried to convert the user鈥檚 requirements into logic equations for the formal specification. The result was a system comprising 150 electronic devices, designed, for example, to handle departure and arrival data and information display. Not only did the system involve a lot of parts and, subsequently, a lot of control programs, but all these programs had to work together so that the departure and arrival data could be displayed on information screens.
Hall thinks that by creating a formal specification the designers have transformed the process. And it appears that this deeper understanding has translated into a more reliable system, with only 150 faults reported during the past two years, which Hall points out is significantly fewer than on many comparable projects.
Is it valid?
But it is not only at the specification stage that formal methods work. Some projects also use a technique called formal validation 鈥� a process that uses mathematical proof to ensure that the program accurately implements the specification.
This proof is rather like the kind of mathematical inference you do in school to prove that the angles of a triangle all add up to 180 degrees. Because the formal specification languages (and some programming languages such as occam) are based on the mathematics of changes of state (the position of switches inside the chip), researchers have found mathematical rules that programs satisfy, rather like the rules discovered by Euclid and his friends for proving facts about triangles and squares.
For safety critical systems, mathematical proofs are the only way to ensure meeting the high levels of confidence demanded by international standards. Most software is still tested rigorously 鈥� putting the program through its paces under various circumstances and then extrapolating to predict whether or not a bug is going to be a nuisance. But to measure a 10鈭�9 probability of failure during an hour of running means that the poor tester must test for more than 114 000 years. This is clearly not feasible, yet 鈥渆xtrapolating from feasible amounts of testing is dangerous鈥� according to Rick Butler of NASA鈥檚 Langley Research Center. Butler believes there is always a chance that the software will fail.
The potential hazards of extrapolation were exposed by the much-publicised bug found in Intel鈥檚 Pentium processor last year. Before launching the Pentium, Intel tested it very rigorously. This involved running a variety of software applications on the processor, as well as checking independently the answers to millions of arithmetical calculations with random inputs. Despite finding evidence of the bug (too late in the design to correct it without significant delay to the launch), they estimated that it would only show up once every 27 000 years.
The vagaries of this process of extrapolation, however, soon became all too clear when another study carried out by IBM estimated that the bug could show up as often as once every 24 days. The major difficulty here is measuring how a typical software program will use the microprocessor 鈥� you just never know for sure. The Pentium bug has since been traced to an error in the software that controls the switching on the chip.
No one will ever know if a formal validation would have made it easier to spot the problem, but other studies suggest that bugs of this kind can be detected during such a design process. In 1990, Inmos (now SGS Thomson) worked with Oxford University鈥檚 programming research group to develop specialised electronics for the T800 transputer chip that was designed to deal with arithmetic. The design phase relied on formal methods, and during the specification a number of errors were found and corrected.
More recently, work by Steven Miller, a researcher at Rockwell International based in Iowa, and Mandayam Srivas, a researcher at SRI International, the Californian consultancy, showed how a more formal approach to design could significantly reduce errors in the design of a processor. They presented their results from using a formal approach to designing and validating the control software for the Rockwell AAMP5 processor last April at a workshop in Boca Raton, Florida.
The chip, which is part of a family that has already been used in products such as the Boeing 757 and Boeing 767 Autopilot Flight Director System and Navstar Global Positioning System, has around 500 000 transistors. This made it a good candidate for testing the efficiency of a formal validation using the Prototype Verification System or PVS. This system, which was developed at SRI, provides computer support for formal specification and proof-checking.
The project lasted 20 months, including a 5-day training course when Rockwell engineers were introduced to PVS. This involved learning the logical language for specification and how to do the mathematical proofs with the automatic proof tool. The mathematical rules of programming are programmed into the proof-checker and, at the press of a button, the proof tool will apply the selected rule. It鈥檚 a tedious job and you might well prove something you don鈥檛 want to know, but at least it should pick up all errors.
After the training, the first task was to specify the assembly language that programmers would use to program the finished processor. This meant describing in logical equations what each command of the assembly language should do. Once the language had been specified, the next stage was to prove that it would behave as expected under the chip鈥檚 electronic control. What makes it difficult is that a simple instruction in assembly language is carried out on the chip by changing many switches and exchanging much more data than an assembly programmer needs to know. The basic approach to proving that the assembly language programs will work as expected followed a similar route to the cash register example. Only in this instance there were many small steps involved.
This is a tedious task. In fact, it is the perfect job for a computer. Some programs are designed to help with this kind of proof. Miller and Srivas chose PVS because it consists 鈥渙f a powerful collection of inference steps that can be used to reduce a proof goal to simpler subgoals that can be discharged automatically鈥�. All the engineers needed to do was to start with the 鈥渁nswer鈥� and then decide which rule to apply.
PVS will follow these rules, proving each one of the equations. The program also splits the proof into several smaller proofs 鈥� or subgoals 鈥� which can be worked on separately. In the case of the command for copying data from one location to another, for example, the engineer would need to prove that the data in all other memory locations remains unchanged. This is achieved by a separate proof that ensures that for each memory location the data remains unchanged. After many such little steps, the proof ends when all the subgoals are self-evident, for example: 1=1. This way the engineers linked the assembly language instructions to the chip鈥檚 electronic signals and then proved important technical details, for example, that the correct signals were sent for when the chip was turned on.
One of the biggest surprises that emerged from the project and a strong point in favour of formal specifications was that the specification on its own revealed errors in the processor design that had not been picked up by the traditional design techniques used in the original chip.
Miller and Srivas say that the formality encourages people drawing up specifications to 鈥渓ook in the corners鈥� and think about unusual conditions which are often the source of errors. The engineers found two errors just by completing the specification 鈥� the sort of errors that would mean the processor would produce the wrong result.
But even better was the ease with which the team discovered two errors that had been deliberately but secretly inserted in the code and these emerged during the proving stage. One error was designed to be difficult to detect by standard testing procedures while the other was a genuine error that had been discovered by traditional testing but not until the AAMP5 had gone to fabrication. Using PVS, the engineers not only found them but were able to identify the source of error 鈥� something that is difficult with testing alone.
Typically, a single failed test signals error without suggesting a cause and many more tests are needed to isolate the problem. With formal specification, the fact that there was a problem and its cause could both be identified at the proving stage which in a real development would happen before the chip was built.
With such good results, it may come as a surprise that software developers are still reluctant to use formal methods. One of the main reasons cited for not using them is the cost. Defining how best to specify and verify complex systems can be difficult and time-consuming. The cash register was easy, but for a real system like the air traffic control system designed by Praxis the specification took over 1500 days. Miller and Srivas agree with Hall, however, and argue that the advantages of a formal approach, like the one they used for the AAMP5, outweigh such disadvantages.
It is not, however, only the cost that puts people off using formal methods, it is the sheer boredom. 鈥淟ong proofs have very little intrinsic interest,鈥� says Michael Goldsmith, director of Formal Systems (Europe) which is developing an automated proof-checker that helps designers get their specifications and implementations right 鈥� a process that up till now has relied on some poor person writing out the equations and working through the proofs.
The proof-checker is called FDR which stands for Failures, Divergences, Refinement and is targeted specifically at systems designed to carry out processing in parallel. Such systems are horrendously difficult to get right because so much is going on at once 鈥� think of a working telephone exchange which must cope with hundreds of activities from dialling and redialling to switching and hanging up. And they are even more difficult and tedious to describe in a mathematical form.
But Goldsmith believes tools such as FDR and PVS offer hope for poor mathematicians assigned to a software design project incorporating formal methods. With such tools under test, along with increasing complexity in software, how much longer can developers of complex or safety-critical systems avoid using formal specifications and proofs? As Hall points out: 鈥淭he question software engineers should be asking about formal methods is not whether to use them, but how best to benefit from them as part of a complete software engineering approach.鈥� (see Diagram)
