Title :
Some Problems in Certifying Microprograms
Author :
Leeman, George B., Jr.
Author_Institution :
Department of Computer Science, IBM Thomas J. Watson Research Center
fDate :
5/1/1975 12:00:00 AM
Abstract :
A hypothetical computer is described, and procedures are indicated for showing the correctness of its microprogram. The underlying method used is that of Birman [1]. However, the computer discussed has some realistic characteristics not shared by the machine treated in [1], and the details of the microcode validation are complicated by this fact. A formal technique for partitioning the proof is presented and illustrated with examples.
Keywords :
Program correctness, algebraic simulation, abstract program, microprogramming, commutative diagram, theorem proving.; Certification; Commutation; Computational modeling; Computer simulation; Data flow computing; Emulation; Manuals; Microprogramming; Programming profession; Read-write memory; Program correctness, algebraic simulation, abstract program, microprogramming, commutative diagram, theorem proving.;
Journal_Title :
Computers, IEEE Transactions on
DOI :
10.1109/T-C.1975.224258
