An Algebraic Approach for Compiling Real-Time Programs

Compiler Verification has been identified as a vital process in the implementation of correct safety-critical systems. We extend here Hoare's refinement-algebra approach to compilation in order to include real-time languages in which processes interact asynchronously via communication queues. The existence of unique fixed-points is exploited to verify the implementation of crucial operators such as asynchronous input, delay and timeout.