Specification and Verification of Real-Time Behaviour Using Z and RTL

Real-Time Logic is a formal notation for reasoning about temporal behaviour. Z is a general purpose specification language, but lacks explicit features for expressing real-time constraints. We show how these complementary methods can be formally unified. An approach to verification of real-time properties by deriving temporal information directly from the specification is then described.

• Type: Conference
• Year: 1992
• Where: FTRTFT
• Authors: Colin J. Fidge
• Keywords: Formal Methods, FTRTFT 1992, Purpose Specification Language, Real-Time Logic, Temporal Behaviour