A real-time refinement calculus that changes only time

The behaviour of a real-time system that interacts repeatedly with its environment is most succinctly specified by its possible traces, or histories. We present a way of using the refinement calculus for developing real-time programs from requirements expressed in this form. Our trace-based specification statements and target language constructs constrain the traces of system variables, rather than updating them destructively like the usual state-machine model. The only variable that is updated is a special current-time variable. The resulting calculus allows refinement from formal specificationswith hard real-time requirements, to high-level language programs annotatedwith precise timing constraints.