An approach to extending Object-Z with real-time

This paper introduces Real-Time Object-Z, a language with real-time extensions to Object-Z, and describes the characters of real-time system: delay, timeout and multithread. Real-Time Object-Z consists two parts: functional specification and filter specification. The both for any time critical system can be developed with two parts. Functional specification developed with Object-Z formerly can be reused. The main benefit is that it is convenient to deal with the timing variables defined in the specification developed with our approach. The effective specification after applying filter part to functional part holds the form of specification developed with Object-Z. Hence, the specification can benefit from existing reasoning systems or inference rules potentially. Using our approach, we can develop real-time specification and reason about the real-time properties conveniently.