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 possible traces, or histories. We present way using the refinement calculus for developing programs from requirements expressed in this form. Our trace-based specification statements and target language constructs constrain traces variables, rather than updating them destructively like usual state-machine model. only variable updated special current-time variable. resulting allows formal specificationswith hard requirements, to high-level annotatedwith precise timing constraints.