Specifying Temporal Requirements for Distributed Real-Time Systems in Z

Andrew Coombes

John McDermid

Department of Computer Science,
University of York,
Heslington,
YORK,
Y01 5DD

ABSTRACT

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 would seem to provide this form of requirement appear to be targeted at specifying communication protocols. While it is possible to adapt these methods for simple timeliness properties, their use for describing constraints on distributed systems would be impractical

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 facilitates the specification of distributed systems. A formal basis for the toolkit is given, together with justification for the features of the model of time that has been adopted.

1. Introduction

In the field of safety-critical systems, there is a growing awareness of the need to specify systems formally (this awareness is manifested in the interim defence standard DEF-STAN 00-55 [MoD91], which mandates the use of formal methods in safety-critical systems). It has also been recognised that the specification of such systems should not merely describe the functionality of the system, but encompass other properties, such as timeliness [McDermid90, Leveson90].

This paper explores the possibility of specifying temporal properties of systems in the Z specification language [Spivey89]. Z is utilised here as it is one of the more widely used specification languages currently available, and it benefits from a relatively well-defined semantics (as given in [Spivey88]) as well as widespread tool support. Although suggestions have been made for approaches where time can be added to Z (specifically [Bowen86, Duke89]), these are more suitable for protocol specification rather than distributed systems, as they lack the means to represent distributed clocks.

The approach to temporal specification described here uses constraints upon histories of variables to describe possible timeliness behaviours of the system. A history of a given variable is represented as a mapping from (non-overlapping) intervals of time to values of the type of the variable. Using intervals in this way permits, amongst other things, easier identification of events (i.e. the times at which a variable holding a specific value becomes true and then false). The concept of time grids (conceptual clocks of differing granularity)