Based on a systematic survey and analysis of the use of formal methods in the development of a dozen industrial applications, we summarize the methods being used, characterize the styles of industrial usage, and provide recommendations for evolutionary enhancements to the technology base of formal methods. The industrial applications ranged from reverse engineering to system certification; code scale ranges from 1 KLOC to 10 KLOC's. Applications included a software infrastructure for oscilloscopes; a shutdown system for a nuclear generating station; a train protection system; an airline collision avoidance system; an engine monitoring system for shipboard engines; attitude control of satellites; security properties of both a smartcard device and a network; arithmetic units; transaction processing; a real-time database for a medical instrument; and a restructuring program for COBOL.>

The STATEMATE system uses a state transition formalism embodied in activity and control charts and supported by simulation, analysis, and documentation tools. The authors describe its application to an automobile cruise control system, emphasizing the methodology lessons of the case study. It is concluded that the strength of the STATEMATE approach lies in the emergence of a set of methods that can be used to construct an incremental system design One possible way to view the design process is as a top-down method where a functional approach is intermixed with the analysis of system functions at each level. It is argued that a design produced using a behavioural methodology for the expressed purpose of simulation will be considerably different from a design produced using a functional method. A strong feature of STATEMATE as a representative of the class of CASE systems is its simulation capability. >

A. Joe Turner

It is becoming increasingly important that communication protocols be formally specified and verified. This paper describes a particular approach–the state transition model–using a collection of mechanically supported specification and verification tools incorporated in a running system called AFFIRM. Although developed for the specification of abstract data types and the verification of their properties, the formalism embodied in AFFIRM can also express the concepts underlying state transition machines. Such models easily express most of the events occurring in protocol systems, including those of the users, their agent processes, and the communication channels. The paper reviews the basic concepts of state transition models and the AFFIRM formalism and methodology and describes their union. A detailed example, the alternating bit protocol, illustrates varous properties of interest for specification and verification. Other examples explored using this formalism are briefly described and the accumulated experience is discussed.

How can one organize the understanding of complex algorithms? People have been thinking about this issue at least since Euclid first tried to explain his innovative greatest common divisor algorithm to his colleagues, but for current research into verifying state-of-the-art programs, some precise answers to the question are needed. Over the past decade the various verification methods which have been introduced (inductive assertions, structural induction, least-fixedpoint semantics, etc.) have established many basic principles of program verification (which we define as: establishing that a program text satisfies a given pair of input-output specifications). However, it is no coincidence that most published examples of the application of these methods have dealt with "toy programs" of carefully considered simplicity.Experience indicates that these "first generation" principles, with which one can easily verify a three-line greatest common divisor algorithm, do not directly enable one to verify a 10,000 line operating system (or even a 50 line list-processing algorithm) in complete detail. To verify complex programs, additional techniques of organization, analysis and manipulation are required. (That a similar situation exists in the writing of large, correct programs has long been recognized -- structured programming being one solution.)This paper examines the usefulness of correctness-preserving program transformations (see [6]) in structuring fairly complex correctness proofs. Using our approach one starts with a simple, high-level (or "abstract") algorithm which can be easily verified, then successively refines it by implementing the abstractions of the initial algorithm to obtain various final, detailed algorithms. In Section 2 we introduce the technique by deriving the Deutsch-Schorr-Waite list-marking algorithm [14]. Our main example is the more complex problem of verifying bounded-workspace list-copying algorithms: Section 3 defines the issues, Section 4 presents the key intermediate algorithm in detail and Section 5 considers three of the most complex (published) implementations of list-copying, one of which is discussed in detail. In Section 6 we make some general remarks on program verification and the relevance of our results to the (larger) field of program correctness; Section 7 mentions some related work.

The verification rules proposed by Hoare are an example of a system which can serve as the basis for a mathematical theory of partial correctness of programs. The purpose of this paper is to extend the previously developed basic theory by (i) defining alternative verification systems and comparing them with the Hoare rules, (ii) deriving several types of useful rules from the basic systems, (iii) showing an ordering on verification systems, (iv) discussing how semi-interpreted program schemas play the role of theorems in a more fully developed theory, (v) formulating a notion of correctness-preserving program transformations and giving a procedure for their use. These extensions provide a more flexible and efficient methodology for proving partial correctness of programs and point to the potential of a mathematical theory which effectively organizes knowledge about programs.

Errors, inconsistencies, or confusing points are noted in a variety of published algorithms, many of which are being used as examples in formulating or teaching principles of such modern programming methodologies as formal specification, systematic construction, and correctness proving. Common properties of these points of contention are abstracted. These properties are then used to pinpoint possible causes of the errors and to formulate general guidelines which might help to avoid further errors. The common characteristic of mathematical rigor and reasoning in these examples is noted, leading to some discussion about fallibility in mathematics, and its relationship to fallibility in these programming methodologies. The overriding goal is to cast a more realistic perspective on the methodologies, particularly with respect to older methodologies, such as testing, and to provide constructive recommendations for their improvement.

Backtracking is a well-known technique for solving combinatorial problems. It is of interest to programming methodologists because 1) correctness of backtracking programs may be difficult to ascertain experimentally and 2) efficiency is often of paramount importance. This paper applies a programming methodology, which we call control structure abstraction, to the backtracking technique. The value of control structure abstraction in the context of correctness is that proofs of general properties of a class of programs with similar control structures are separated from proofs of specific properties of individual programs of the class. In the context of efficiency, it provides sufficient conditions for correctness of an initial program which may subsequently be improved for efficiency while preserving correctness.

This paper extends the predicate calculus formalization of the partial correctness properties of programs (Ki, Go) to include the preservation of correctness under program transformations. The general notion of "program transformations which preserve properties" is fundamental to the theory of programming and programming languages. In the context of proofs of program correctness, transformations which preserve correctness can be used to improve less efficient, but easier to prove, programs. The basic argument in the use of correctness-preserving program transformations (hereafter CPTs) is:Assume that G is a program (with attached assertions) which has been proved correct with respect to some input-output relation Ain-Aout. Now suppose that S is some part of G, e.g. an expression, assertion, statement, etc., which is to be replaced by some other such part S' to produce the program G'. The goal is to prove that G' is also correct with respect to Ain-Aout and therefore the replacement preserves overall program correctness. Moreover, if the replacement has only a local effect, e.g. the body of a loop, then the proof of correctness-preservation should be restricted to that part of the program affected by the replacement.Section 2 reviews the current paradigm for proving program correctness. An example in section 3 illustrates CPTs in a sequence of improvements on a correct and simple, but inefficient, initial program. In section 4, the formalization of partial correctness properties of programs is recast as a semantic language definition using Knuth's semantic method (Kn1). This formalization is then used in section 5 to describe the mechanics of performing CPTs. In section 6, several questions about the formalization of sections 4 and 5 are discussed and a generalization is proposed. Finally, section 7 returns to a concrete example and suggests that the most effective use of CPTs is by identification of schematic forms. Related work is mentioned in section 8.

“Program verification” is generally defined as the process of ascertaining and demonstrating that a program is correct, i.e., that a program satisfies a given set of specifications. The most common method of verifying a program is by testing, the process of executing a program for a set of selected inputs and inferring from the results of those executions that the program is correct for all possible inputs.

Examines the theoretical and practical role of testing in software development. The authors prove a fundamental theorem showing that properly structured tests are capable of demonstrating the absence of errors in a program. The theorem's proof hinges on our definition of test reliability and validity, but its practical utility hinges on being able to show when a test is actually reliable. The authors explain what makes tests unreliable (for example, they show by example why testing all program statements, predicates, or paths is not usually sufficient to insure test reliability), and they outline a possible approach to developing reliable tests. They also show how the analysis required to define reliable tests can help in checking a program's design and specifications as well as in preventing and detecting implementation errors.