|
|
|---|
|
|
|
|---|
R. S. Boyer and J S. Moore, “On
Why It Is Impossible to Prove that the BDX930 Dispatcher Implements a
Time-Sharing System”, in Sections 14 and 15 of P.M. Melliar-Smith,
K. Levitt, R. Schwartz, R. Boyer, J Moore, D. Hare, R. Shostak, M. Moriconi,
M. Green, and W.D. Elliot, Investigation, Development, and Evaluation of
Performance Proving for Fault-Tolerant Computer Final Report, covering the
period September 1978 to June 1982, SRI, July 1982.
Relevance: operational semantic model of (a
fragment) of a 1970s flight control computer
Boyer and Moore's formalization of a subset of the instruction set of the Bendix BDX930 flight control computer is reported in this document. The document is part of the Final Report for the Software Implemented Fault Tolerance (SIFT) project of SRI, sponsored by the National Aeronautics and Space Administration, Langley Research Center, Hampton, Va 23665. Section 14 explains why it was impossible to verify that the code for the SIFT dispatcher implemented a time-sharing system; Section 15 contains the 30 page listing of the operational semantics for the BDX930 fragment in question, written in the logic of Thm/Nqthm. The two sections do not contain dates. The whole report covers the period 1978 through 1982. Boyer and Moore left SRI in 1981. The BDX930 work was probably done in 1979 or 1980 as it was influential in the evolution of Thm to Nqthm, as noted in operational-semantics-5__history-etc.