Proceedings

The meaning of software reliability and the problems involved in attaining reliable software are examined from three perspectives: customer, producer, and user. The impact of reliable software on the public at large is discussed, emphasizing the ...

So-called “guarded commands” are introduced as a building block for alternative and repetitive constructs that allow non-deterministic program components for which at least the activity evoked, but possibly even the final state, is not necessarily ...

This paper discusses the serious need for improved management methods and software development technology to support the production of truly reliable software and presents experience gained on TRW's Site Defense Program in addressing that need.

The ...

The language in which programs are written can have a substantial effect on their reliability. This paper discusses the design of programming languages to enhance reliability. It presents several general design principles, and then applies them to ...

The programming language PASCAL is assessed in the light of “reliable programming” and with the background of five years of experience with the language. Some features are selected to point out remaining problems, either inherent or specific, from which ...

The cost of a change to a large software system is often primarily a function of the size of the system rather than the complexity of the change. One reason for this is that programs which access some given data structure must operate on it using ...

This paper describes the structure and expounds the underlying motivations of the 'Testing System' which is presently being designed and experienced in testing the Honeywell GCOS Level 62 operating system. TS is a hierarchical system in which two main ...

Software quality enhancement can be achieved in the near term through use of a systematic program testing methodology. The methodology attempts to relate functional software testcases with formal software specifications as a means to achieve ...

Automated tools and structured programming techniques are in use on a variety of scientific and business application programming projects within the McDonnell Douglas Corporation. An examination of the resulting programs reveals certain development and ...

The main purposes in writing this paper are to discuss the importance of formal specifications and to survey a number of promising specification techniques. The role of formal specifications both in proofs of program correctness, and in programming ...

Dijkstra suggests in his “Notes on Structured Programming” that program schema and theorems about their correctness may describe the way that programmers understand programming. This paper follows up his suggestion by describing a general model for ...

This paper is a preliminary report on an experiment in applying Floyd's method of inductive assertions to the compiler correctness problem. Practical postfix translators are considered, and the semantics of source and object languages are characterized ...

This paper summarizes some recent experience in analyzing and eliminating sources of error in the design phase of large software projects. It begins by pointing out some of the significant differences in software error incidence between large and small ...

We distinguish the activity of writing large programs from that of writing small ones. By large programs we mean systems consisting of many small programs (modules), possibly written by different people.

We need languages for programming-in-the-small, ...

This paper deals with the problem of reliability in a hardware/software system. More specifically it deals with the strategy used to achieve reliability in a particular hardware/software system built by the author and his colleagues at Carnegie-Mellon ...

Recent investigations on the use of automation to realize the twin objectives of cost reduction and reliability improvement for computer programs developed for the U. S. Air Force are reported. The concepts of reliability and automation as they pertain ...

We present the germ of an idea for automatically correcting logical errors in programs by manipulating the invariants of the program. An invariant tree is defined, and we show how it can be used to change the program in order to guarantee correctness.

...

The paper investigates methods for applying an online interactive verification system designed to prove properties of PASCAL programs. The methodology provides techniques for developing a debugged and verified version starting from an incomplete program...

We attempt to extract from any program loop its “Most General Invariant” in order to either prove its correctness, including termination, or disprove it and propose corrections.

This paper discusses how structured programming methodology has been introduced into a large production programming organization using an integrated but flexible approach. It next analyzes the advantages and disadvantages of each component of the ...

Much of the software developed to support engineering design calculations is produced by persons whose primary job skill is not that of computer scientist. Software validation techniques suitable for use by these engineer-programmers have been under ...

The book, The Mythical Man-Month, Addison-Wesley, 1975 (excerpted in Datamation, December 1974), gathers some of the published data about software engineering and mixes it with the assertion of a lot of personal opinions. In this presentation, the ...

This paper discusses actual software reliability data obtained in an on line real time environment. The measures used are the reliability function R(t) and the mean time between software errors MTBSE. How to measure the operational data of R(t) or MTBSE ...

A system is considered in which switching takes place between sub-systems according to a continuous parameter Markov chain. Failures may occur in Poisson processes in the sub-systems, and in the transitions between sub-systems. All failure processes are ...

A many-state Markov model has been developed for the purpose of providing various performance criteria for computer software. The software system under consideration is assumed to be fairly large, of the order of 10⁵ words of code, so that statistical ...

A technique is presented whereby a significant amount of program validation can be done simply by exercising the program components in a model environment provided by a finite state machine, specially built to characterise the real environment of that ...

The current approach for testing a program is, in principle, quite primitive. Some small sample of the data that a program is expected to handle is presented to the program. If the program produces correct results for the sample, it is assumed to be ...

SELECT is an experimental system for assisting in the formal systematic debugging of programs. It is intended to be a compromise between an automated program proving system and the current ad hoc debugging practice, and is similar to a system being ...