Specifying temporal requirements for distributed real-time systems in Z

It is becoming widely accepted that along with the formal specification of functional properties it is necessary, in some systems, to provide a specification of timeliness properties. Unfortunately, the main methods which seem to provide this form of requirement appear to be based solely on a global model of time, which are inappropriate for the specification of asynchronous distributed systems. This paper introduces a set of definitions for the Z specification language which enables timeliness properties to be represented formally. The toolkit provides a method of framing the temporal specifications, which enables these specifications to be looked at from multiple viewpoints; a feature which allows one to look at the time domain at different levels of abstraction, and to represent the effects of multiple unsynchronised clocks. A formal basis for the toolkit is given, together with justification for the features of the model of time that has been adopted