Title: Encoding Temporal Logics in Executable Z: 
       A Case Study for the ZETA System
Authors: Wolfgang Grieskamp, Markus Lepper

Abstract:

The ZETA system is a Z-based tool environment for developing
formal specifications. It contains a component for executing
the Z language based on the implementation technique of
concurrent constraint resolution. In this paper, we present a
case-study for the environment, by providing an executable encoding
of temporal interval logics in the Z language. As an
application of this setting, test-case evaluation of trace-producing
systems on the base of a formal requirements specifications is envisaged.