Formal Analysis of Concurrent Real-Time Requirements Models

This report demonstrates the use of modal and temporal logic to analysis the functional and safety requirements of concurrent real-time systems. Our research is based on the integrated method: Hazard and Operability Studies;Ward and Mellor Essential Models; and the Temporal Calculus of Communicating Systems to model and analyse real-time control systems. In particular, we discuss the interplay between traditional hazard analysis techniques and formal methods and their associated analyses in the context of an integrated model. The approach is illustrated by a small but realistic industrial case study.