Computer-aided development of a real-time program

The refinement calculus is a well-established theory for formal development of imperative program code and is supported by a number of automated tools. Via a detailed case study, this article shows how refinement theory and tool support can be extended for a program with real-time constraints. The approach adapts a timed variant of the refinement calculus and makes corresponding enhancements to a theorem-prover based refinement tool