Producing Correct Software

by Rodger Knaus, Instant Recall, Inc. and James Wentworth, Advanced Research Team, Turner- Fairbank Highway Research Center, FHWA

This web page accomplishes the following:

• Defines software correctness.
• Suggests a list of concrete tasks and problems, which, particularly when used together, can improve software correctness.
• Introduces techniques to solve these problems.

More detailed information about techniques introduced here will appear later in subdocuments linked to this document.

Introduction
Software development is a relatively new activity being utilized by an ancient profession. Construction and roadway engineering began in prehistoric times, and over time the industry has raised the standards in design, construction, and the documentation of practice. Through modernizing and improving design, construction, and maintenance, new approaches and technologies have been incorporated into civil engineering practice. Many of the new tools and technologies did not initially achieve the levels of reliability and standardization that the civil engineering profession demanded. Regrettably, software development and computer programs fall into this category.

Software planning and development should emulate construction project planning, design, and construction, integrating testing and evaluation. The end result will be more reliable software and more reliable transportation systems.

Software developers must use tools for improving software and catching design problems at an early stage of the software development life cycle, when fixing those problems is relatively cheap and easy. These tools must be easy to use for both the engineer responsible for software development and for the software developer. The software should not be designed for just those individuals with unusual mathematical training.

In traditional software engineering, developers claim that testing is an integral part of the design and development process. However, as programming techniques become more and more advanced and complex, there is little consensus on what testing is necessary or how to perform it. Furthermore, many of the procedures that have been developed for verification and validation (V&V) are so poorly documented that only the originator can reproduce the procedures. The complexity and uncertainty of these procedures has led to the inadequate testing of software systems (even operational systems). As software becomes more complex, it becomes more difficult to produce correct softwarežand the penalties for errors will increase.

Definition of Software Correctness
This document is an introduction to some techniques for producing correct software. Correct software must accomplish the following:

• G1: Compute accurate results.
• G2: Operate safely, and causes the system containing the software to operate safely.
• G3: Perform the tasks required by the system containing the software, as explained in the software specifications.
• G4: Achieve these goals for all inputs.
• G5: Recognize inputs outside its domain.

These goals will be referred to collectively as "software correctness," and achieving these goals will be referred to as "achieving correctness (in software)" or as the "correctness problem."

Common Elements for All Correctness Problems
Designing and building software is a branch of engineering. As such, the following is true:

• Scientific and engineering knowledge is used to produce designs that satisfy the requirements G1-G5.
• Theory is used to check the completed design.
• Like other creations of engineering, the end product (the software) must be tested before it is known to work.

As with other designed objects, having completely reliable computer software is not possible with current technology. However, there are some techniques that engineers in other areas use to increase reliability in general, which appear likely to increase software reliability:

• Employing careful management and work practices during design and construction.
• Using theory to check completed designs.
• Designing alarms and safety devices into the deployed device.

Most current software standards have focused on management and work on software projects rather than focusing on whether the software will work safely and reliably. Management and work standards are valuable, but these standards by themselves do not guarantee correct software for the following reasons:

• It is impossible to enforce the work standards 100 percent of the time.
• Software developers make mistakes even when following the standards.

Therefore, software developers need to accomplish the following:

• Theoretically establish correctness of the currently built program (usually assuming that underlying hardware and support software is correct).
• Make software self-checking and self-correcting.

These topics are presented in subpages:

• Formal methods to establish correctness (under development).
• Making software self-checking and self-correcting.

[T O C] | [N E X T]