A formal model of real-time program compilation

Abstract. Program compilation can be formally defined as a sequence of equivalence-preserving transformations, or refinements, from highlevel language programs to assembler code. Recent models also incorporate timing properties, but the resulting formalisms are prohibitively complex. Here we take advantage of a new, simple model of real-time refinement to present a straightforward formalism for compilation that incorporates real-time constraints.