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.
Author and article information
Software Verification Research Centre,
Department of Computer Science,
The University of Queensland,
Queensland 4072, Australia.