Adding real-time filters to object-oriented specification of time critical systems

We describe Real-Time Object-Z (RTOZ), a language with real-time extensions to Object-Z, and describe informally its semantics. The novelty of our approach lies in the minimal set of syntactic extensions to Object-Z and in the introduction of real-time filters for the separation of real time constraints from the functional specification of objects. Both the functional specification and filter specification for any time critical system can be developed using the syntax of RTOZ. The semantics of RTOZ provides a consistent mapping between the classes in an Object-Z specification and their corresponding real-time constraints. We illustrate the expressive power of RTOZ with a case study