Temporal logic and Z specifications
Roger Duke, Graeme Smith · 1990
The Z specification language can be used to capture liveness properties of state transition systems such as those used to specify communications protocols. The specification of such systems involve temporal concepts such as "eventually" and "always". In this paper we extend standard Z to include the temporal logic operators so as to provide a powerful notation for discussing the liveness of state transition systems. By way of an illustration of the ideas involved, we look at a state transition model for an alternating bit protocol, and compare the specifications of liveness in standard Z and Z enhanced with the temporal logic notation. Keywords and Phrases : liveness, protocols, temporal logic, Z CR Categories : c.2.2, d.2.1, d.2.4, f.3.1 1 Introduction In Duke et al [2, 3] the Z specification language [7, 10] was used to model communications protocols as event-driven [9] state transition systems [11]. The Z language, developed at the Programming Research Group of Oxford University ...