Specification Language.

The specification language SL of ProCoS I divides a specification into a trace part and a state part. This division is in principle closely related to ideas in UNITY [14], Back's action systems [2] and Lamport's TLA [26]. The state part corresponds to an iterative program or action system, and the trace part to a behavioural specification of that program.

The integration of time into the specification language encompasses the following aspects:

• The relations between the duration calculus and the specification language are explored. [18] describes the step from DC to switching circuits which are close to SLtime.

• In cooperation with Lyngby we shall evaluate case studies that indicate which timing properties are needed and how they can be expressed in different existing time calculi. One such study, a railway crossing, is presented in [37].

• Work at Oxford indicates that timing requirements can be classified into those stating lower bounds (``waits'') and others stating upper bounds (``speed-ups''). We wish to investigate whether taking these two aspects separately leads to simpler calculi.

A first version of the timed specification language is proposed in [37].