Adding linear temporal logic with clocks to Object-Z
用带时钟变量的线性时态逻辑扩充Object-Z*

Object-Z, an extension to formal specification language Z, is good for describing large scale object-oriented software specification. While Object-Z has found application in a number of areas, its utility is limited by its inability to specify continuous variables and real-time constraints. Linear temporal logic can describe real-time system, but it can not deal with time variables well and also can not describe formal specification modularly. This paper extended linear temporal logic with clocks(LTLC) and presented an approach to adding linear temporal logic with clocks to Object-Z. Extended Object-Z with LTLC, a modular formal specification language, is a minimum extension of the syntax and semantics of Object-Z. The main advantage of this extension lies in that it is convenient to describe and verify the complex real-time software specification.