Engineering topics

Maurer, W. D.

Publications and source records attributed to Maurer, W. D..

3 records

NASA NTRS1977

Proving the correctness of the flight director program EADIFD, volume 1

EADIFD is written in symbolic assembly language for execution on the C4000 airborne computer. It is a subprogram of an aircraft navigation and guidance program and is used to generate pitch and roll command signals for use in terminal airspace. The proof of EADIFD was carried out by an inductive assertion method consisting of two parts, a verification condition generator and a source language independent proof checker. With the specifications provided by NASA, EADIFD was proved correct. The termination of the program is guaranteed and the program contains no instructions that can modify it under any conditions.

Lee, F. J.↗

NASA NTRS1977

An IBM 370 assembly language program verifier

The paper describes a program written in SNOBOL which verifies the correctness of programs written in assembly language for the IBM 360 and 370 series of computers. The motivation for using assembly language as a source language for a program verifier was the realization that many errors in programs are caused by misunderstanding or ignorance of the characteristics of specific computers. The proof of correctness of a program written in assembly language must take these characteristics into account. The program has been compiled and is currently running at the Center for Academic and Administrative Computing of The George Washington University.

Maurer, W. D.↗

NASA NTRS1977

Proving the correctness of a flight-director program for an airborne minicomputer

Program verification procedures are described and used to determine the correctness of a program written for an airborne computer. The basic method relies on the inductive assertion method of Floyd (1967), modified and extended for application to a machine-language situation. Correctness considerations in the flight director program include self-modification, system correctness, executable instructions, overflow, approximate calculations with fractional quantities, and fixed point scaling. An example proof of correctness, which proceeds by proving the correctness of a certain subroutine, is provided.

Maurer, W. D.↗