Issue No. 10 - October (1976 vol. 25)
D.A. Patterson , Department of Computer Science, University of California, Los Angeles, CA and the Data Systems Division, Hughes Aircraft Company
An approach to the development of correct microprograms is to use the methodologies that have been beneficial in the generation of correct user programs, i. e., structured programming, high-level languages (HLL's), and formal program verification using Floyd's inductive assertion method. This paper presents a system that combines these techniques to simplify the design and implementation of correct microprograms for a real microprogrammable computer. It gives some statistics which support our emphasis on generation as well as correctness and some preliminary results on the use of our system.
High-level languages (HLL's), inductive assertions, microprogramming, program correctness, structured programming.
D. Patterson, "Strum: Structured Microprogram Development System for Correct Firmware," in IEEE Transactions on Computers, vol. 25, no. , pp. 974-985, 1976.