Encoding Temporal Logics in Executable Z: A Case Study for the ZETA System

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.

• Type: Conference
• Year: 2000
• Where: LPAR
• Authors: Wolfgang Grieskamp, Markus Lepper
• Keywords: Automated Reasoning, Concurrent Constraint Resolution, LPAR 2000, Temporal Interval Logics, Z-based Tool Environment